src/HOLCF/fixrec_package.ML
changeset 18358 0a733e11021a
parent 17985 d5d576b72371
child 18377 0e1d025d57b3
--- a/src/HOLCF/fixrec_package.ML	Tue Dec 06 06:22:14 2005 +0100
+++ b/src/HOLCF/fixrec_package.ML	Tue Dec 06 09:04:09 2005 +0100
@@ -101,7 +101,7 @@
     val (names, pre_fixdefs) = ListPair.unzip (defs lhss fixpoint);
     
     val fixdefs = map (inferT_axm thy) pre_fixdefs;
-    val (thy', fixdef_thms) =
+    val (fixdef_thms, thy') =
       PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy;
     val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms;