src/Tools/induct.ML
changeset 49748 a346daa8a1f4
parent 49660 de49d9b4d7bc
child 51580 64ef8260dc60
     1.1 --- a/src/Tools/induct.ML	Tue Oct 09 19:24:19 2012 +0200
     1.2 +++ b/src/Tools/induct.ML	Tue Oct 09 20:05:17 2012 +0200
     1.3 @@ -705,15 +705,15 @@
     1.4      fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt)
     1.5        | add (SOME (SOME x, (t, _))) ctxt =
     1.6            let val ([(lhs, (_, th))], ctxt') =
     1.7 -            Local_Defs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
     1.8 +            Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt
     1.9            in ((SOME lhs, [th]), ctxt') end
    1.10        | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
    1.11        | add (SOME (NONE, (t, _))) ctxt =
    1.12            let
    1.13              val (s, _) = Name.variant "x" (Variable.names_of ctxt);
    1.14 -            val ([(lhs, (_, th))], ctxt') =
    1.15 -              Local_Defs.add_defs [((Binding.name s, NoSyn),
    1.16 -                (Thm.empty_binding, t))] ctxt
    1.17 +            val x = Binding.name s;
    1.18 +            val ([(lhs, (_, th))], ctxt') = ctxt
    1.19 +              |> Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))];
    1.20            in ((SOME lhs, [th]), ctxt') end
    1.21        | add NONE ctxt = ((NONE, []), ctxt);
    1.22    in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;