theory TestDef imports Main
keywords "mydef" :: thy_decl
begin

definition "TestDefB a = (a = a)"


ML{*
  val th_A = Simplifier.rewrite (@{context} addsimps [@{thm TestDefB_def}]) @{cterm "TestDef u"}
  val tfrees = Term.add_tfrees (Thm.prop_of th_A)  [];
  val th_A_gen = Thm.generalize (map fst tfrees, [])  ((Thm.maxidx_of th_A) + 1) th_A;
  val tvars = Term.add_tvars (Thm.prop_of th_A_gen) [];
  val th_A_inst = Drule.instantiate_normalize (map (fn x => (x, @{ctyp bool})) tvars,[]) th_A_gen;
*}

ML{*
fun gen_def prep (raw_var, raw_spec) int lthy =
  let
    val ((vars, [((raw_name, atts), prop)]), get_pos) =
      fst (prep (the_list raw_var) [raw_spec] lthy);
    val (((x, T), rhs), prove) = Local_Defs.derived_def lthy true prop;
    val _ = Name.reject_internal (x, []);
    val var as (b, _) =
      (case vars of
        [] => (Binding.make (x, get_pos x), NoSyn)
      | [((b, _), mx)] =>
          let
            val y = Variable.check_name b;
            val _ = x = y orelse
              error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
                Position.here (Binding.pos_of b));
          in (b, mx) end);
    val name = Binding.reset_pos (Thm.def_binding_optional b raw_name);
    val ((lhs, (_, raw_th)), lthy2) = lthy
      |> Local_Theory.define_internal (var, ((Binding.suffix_name "_raw" name, []), rhs));

    val th = prove lthy2 raw_th;
    val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);

        val th_a =  th;
        val tfrees = Term.add_tfrees (Thm.prop_of th_a)  [];
        val th_gen = Thm.generalize (map fst tfrees, []) ((Thm.maxidx_of th_a) + 1) th_a;


    val ([(def_name, [th'])], lthy4) = lthy3
      |> Local_Theory.notes [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];

    val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;



    val _ =
      Proof_Display.print_consts int (Position.thread_data ()) lthy4
        (member (op =) (Term.add_frees lhs' [])) [(x, T)];
  in ((lhs, (def_name, th')), lthy4) end;

val definition_cmd = gen_def  Specification.read_free_spec;

val _ =
  Outer_Syntax.local_theory' @{command_keyword mydef} "constant mydef"
    (Parse_Spec.constdef >> (fn args => #2 oo definition_cmd args));


*}

mydef "TestDefA a = (a = a)"





end