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 31177 c39994cb152a
parent 31174 f1f1e9b53c81 
--- a/src/HOL/Tools/inductive_package.ML	Sun May 17 07:17:39 2009 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Mon May 18 09:48:06 2009 +0200
@@ -454,7 +454,7 @@
     val facts = args |> map (fn ((a, atts), props) =>
       ((a, map (prep_att thy) atts),
         map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
-  in lthy |> LocalTheory.notes Thm.generated_theoremK facts |>> map snd end;
+  in lthy |> LocalTheory.notes Thm.generatedK facts |>> map snd end;
 
 val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
 val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
@@ -849,7 +849,7 @@
       |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
     val (cs, ps) = chop (length cnames_syn) vars;
     val monos = Attrib.eval_thms lthy raw_monos;
-    val flags = {quiet_mode = false, verbose = verbose, kind = Thm.generated_theoremK,
+    val flags = {quiet_mode = false, verbose = verbose, kind = Thm.generatedK,
       alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
       skip_mono = false, fork_mono = not int};
   in
isabelle