# HG changeset patch
# User wenzelm
# Date 1160177467 -7200
# Node ID ac46f01024be8651d8e18e981baf4d531c5bdf80
# Parent  384c5bb713b28a4f570c16c67464538e4ff51ba8
improved LocalDefs.add_def;

diff -r 384c5bb713b2 -r ac46f01024be src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Sat Oct 07 01:31:06 2006 +0200
+++ b/src/Provers/induct_method.ML	Sat Oct 07 01:31:07 2006 +0200
@@ -329,8 +329,8 @@
 fun add_defs def_insts =
   let
     fun add (SOME (SOME x, t)) ctxt =
-          let val ((lhs, def), ctxt') = LocalDefs.add_def (x, t) ctxt
-          in ((SOME (Free lhs), [def]), ctxt') end
+          let val ([(lhs, (_, th))], ctxt') = LocalDefs.add_defs [((x, NoSyn), (("", []), t))] ctxt
+          in ((SOME lhs, [th]), ctxt') end
       | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
       | add NONE ctxt = ((NONE, []), ctxt);
   in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;