src/HOL/Tools/inductive_realizer.ML
changeset 18358 0a733e11021a
parent 18314 4595eb4627fa
child 18708 4b3dadb4fe33
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Dec 06 06:22:14 2005 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Dec 06 09:04:09 2005 +0100
@@ -378,7 +378,7 @@
            REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
              [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
-        val (thy', thm') = PureThy.store_thm ((space_implode "_"
+        val (thm', thy') = PureThy.store_thm ((space_implode "_"
           (Thm.name_of_thm induct :: vs @ Ps @ ["correctness"]), thm), []) thy
       in
         Extraction.add_realizers_i
@@ -426,7 +426,7 @@
            rewrite_goals_tac rews,
            REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
-        val (thy', thm') = PureThy.store_thm ((space_implode "_"
+        val (thm', thy') = PureThy.store_thm ((space_implode "_"
           (Thm.name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
       in
         Extraction.add_realizers_i