Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Fri, 09 Nov 2001 22:50:58 +0100
changeset 12128 25565bbbd246
parent 12127 219e543496a3
child 12129 964f5ffe13d0
tuned;
src/HOL/Tools/inductive_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/inductive_package.ML	Fri Nov 09 22:50:32 2001 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Nov 09 22:50:58 2001 +0100
@@ -858,9 +858,9 @@
     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
     val (cs', intr_ts') = unify_consts sign cs intr_ts;
 
-    val ((thy', con_defs), monos) = thy
+    val (thy', (monos, con_defs)) = thy
       |> IsarThy.apply_theorems raw_monos
-      |> apfst (IsarThy.apply_theorems raw_con_defs);
+      |>>> IsarThy.apply_theorems raw_con_defs;
   in
     add_inductive_i verbose false "" coind false false cs'
       ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
isabelle