# HG changeset patch
# User wenzelm
# Date 1191942632 -7200
# Node ID f38dd8d0a30df2e25489af1898a93c7ac9611e4b
# Parent  2a49fc046dc089d433a714d5eccb8bef93c02806
removed LocalTheory.defs, use plain LocalTheory.def;

diff -r 2a49fc046dc0 -r f38dd8d0a30d src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Tue Oct 09 00:26:56 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Tue Oct 09 17:10:32 2007 +0200
@@ -662,7 +662,7 @@
             (list_comb (rec_const, params @ make_bool_args' bs i @
               make_args argTs (xs ~~ Ts)))))
         end) (cnames_syn ~~ cs);
-    val (consts_defs, ctxt'') = LocalTheory.defs Thm.internalK specs ctxt';
+    val (consts_defs, ctxt'') = fold_map (LocalTheory.def Thm.internalK) specs ctxt';
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
     val mono = prove_mono predT fp_fun monos ctxt''
diff -r 2a49fc046dc0 -r f38dd8d0a30d src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Tue Oct 09 00:26:56 2007 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML	Tue Oct 09 17:10:32 2007 +0200
@@ -468,7 +468,7 @@
         cs' intros' monos' params1 cnames_syn' ctxt;
 
     (* define inductive sets using previously defined predicates *)
-    val (defs, ctxt2) = LocalTheory.defs Thm.internalK
+    val (defs, ctxt2) = fold_map (LocalTheory.def Thm.internalK)
       (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (("", []),
          fold_rev lambda params (HOLogic.Collect_const U $
            HOLogic.ap_split' fs U HOLogic.boolT (list_comb (p, params3))))))