src/HOL/Tools/inductive_package.ML
changeset 25016 2bcac52d7abc
parent 24960 39d1dd215d73
child 25029 3a72718c5ddd
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Oct 12 22:01:56 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Oct 13 17:16:39 2007 +0200
     1.3 @@ -645,7 +645,7 @@
     1.4        space_implode "_" (map fst cnames_syn) else alt_name;
     1.5  
     1.6      val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
     1.7 -      LocalTheory.def Thm.internalK
     1.8 +      LocalTheory.define Thm.internalK
     1.9          ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
    1.10           (("", []), fold_rev lambda params
    1.11             (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
    1.12 @@ -662,7 +662,7 @@
    1.13              (list_comb (rec_const, params @ make_bool_args' bs i @
    1.14                make_args argTs (xs ~~ Ts)))))
    1.15          end) (cnames_syn ~~ cs);
    1.16 -    val (consts_defs, ctxt'') = fold_map (LocalTheory.def Thm.internalK) specs ctxt';
    1.17 +    val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
    1.18      val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
    1.19  
    1.20      val mono = prove_mono predT fp_fun monos ctxt''