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