src/HOL/Tools/inductive_realizer.ML
changeset 23590 ad95084a5c63
parent 23577 c5b93c69afd3
child 24157 409cd6eaa7ea
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Jul 05 20:01:26 2007 +0200
@@ -388,7 +388,7 @@
           [rtac (#raw_induct ind_info) 1,
            rewrite_goals_tac rews,
            REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
-             [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
+             [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
         val (thm', thy') = PureThy.store_thm ((space_implode "_"
           (NameSpace.qualified qualifier "induct" :: vs @ Ps @
@@ -449,7 +449,7 @@
            etac elimR 1,
            ALLGOALS (asm_simp_tac HOL_basic_ss),
            rewrite_goals_tac rews,
-           REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
+           REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
         val (thm', thy') = PureThy.store_thm ((space_implode "_"
           (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy