# HG changeset patch
# User wenzelm
# Date 1138465732 -3600
# Node ID 86eec44dae664fa7b21639a51c30637a3e4110c8
# Parent  ad8bc3e55aa3d23f4af3f41fa7891b16b91aba68
LocalDefs.add_def;

diff -r ad8bc3e55aa3 -r 86eec44dae66 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Sat Jan 28 17:28:51 2006 +0100
+++ b/src/Provers/induct_method.ML	Sat Jan 28 17:28:52 2006 +0100
@@ -342,7 +342,7 @@
 fun add_defs def_insts =
   let
     fun add (SOME (SOME x, t)) ctxt =
-          let val ((lhs, def), ctxt') = ProofContext.add_def (x, t) ctxt
+          let val ((lhs, def), ctxt') = LocalDefs.add_def (x, t) ctxt
           in ((SOME (Free lhs), [def]), ctxt') end
       | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
       | add NONE ctxt = ((NONE, []), ctxt);