Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/inductive_package.ML
changeset 25016 2bcac52d7abc
parent 24960 39d1dd215d73
child 25029 3a72718c5ddd 
--- a/src/HOL/Tools/inductive_package.ML	Fri Oct 12 22:01:56 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Sat Oct 13 17:16:39 2007 +0200
@@ -645,7 +645,7 @@
       space_implode "_" (map fst cnames_syn) else alt_name;
 
     val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
-      LocalTheory.def Thm.internalK
+      LocalTheory.define Thm.internalK
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
          (("", []), fold_rev lambda params
            (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
@@ -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'') = fold_map (LocalTheory.def Thm.internalK) specs ctxt';
+    val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
     val mono = prove_mono predT fp_fun monos ctxt''
isabelle