removed LocalTheory.defs, use plain LocalTheory.def;
authorwenzelm
Tue Oct 09 17:10:32 2007 +0200 (2007-10-09)
changeset 24925f38dd8d0a30d
parent 24924 2a49fc046dc0
child 24926 bcb6b098df11
removed LocalTheory.defs, use plain LocalTheory.def;
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_set_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Oct 09 00:26:56 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Oct 09 17:10:32 2007 +0200
     1.3 @@ -662,7 +662,7 @@
     1.4              (list_comb (rec_const, params @ make_bool_args' bs i @
     1.5                make_args argTs (xs ~~ Ts)))))
     1.6          end) (cnames_syn ~~ cs);
     1.7 -    val (consts_defs, ctxt'') = LocalTheory.defs Thm.internalK specs ctxt';
     1.8 +    val (consts_defs, ctxt'') = fold_map (LocalTheory.def Thm.internalK) specs ctxt';
     1.9      val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
    1.10  
    1.11      val mono = prove_mono predT fp_fun monos ctxt''
     2.1 --- a/src/HOL/Tools/inductive_set_package.ML	Tue Oct 09 00:26:56 2007 +0200
     2.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Tue Oct 09 17:10:32 2007 +0200
     2.3 @@ -468,7 +468,7 @@
     2.4          cs' intros' monos' params1 cnames_syn' ctxt;
     2.5  
     2.6      (* define inductive sets using previously defined predicates *)
     2.7 -    val (defs, ctxt2) = LocalTheory.defs Thm.internalK
     2.8 +    val (defs, ctxt2) = fold_map (LocalTheory.def Thm.internalK)
     2.9        (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (("", []),
    2.10           fold_rev lambda params (HOLogic.Collect_const U $
    2.11             HOLogic.ap_split' fs U HOLogic.boolT (list_comb (p, params3))))))