--- a/src/Tools/induct.ML Wed Jun 22 10:09:20 2016 +0200
+++ b/src/Tools/induct.ML Wed Jun 22 10:40:53 2016 +0200
@@ -725,7 +725,7 @@
fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt)
| add (SOME (SOME x, (t, _))) ctxt =
let val ([(lhs, (_, th))], ctxt') =
- Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt
+ Local_Defs.define [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt
in ((SOME lhs, [th]), ctxt') end
| add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
| add (SOME (NONE, (t, _))) ctxt =
@@ -733,7 +733,7 @@
val (s, _) = Name.variant "x" (Variable.names_of ctxt);
val x = Binding.name s;
val ([(lhs, (_, th))], ctxt') = ctxt
- |> Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))];
+ |> Local_Defs.define [((x, NoSyn), ((Thm.def_binding x, []), t))];
in ((SOME lhs, [th]), ctxt') end
| add NONE ctxt = ((NONE, []), ctxt);
in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;