src/HOL/Tools/inductive_realizer.ML
changeset 26481 92e901171cc8
parent 26477 ecf06644f6cb
child 26535 66bca8a4079c
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Mar 29 19:14:00 2008 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Mar 29 19:14:03 2008 +0100
     1.3 @@ -396,9 +396,8 @@
     1.4             REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
     1.5               [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
     1.6                DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
     1.7 -        val (thm', thy') = PureThy.store_thm ((space_implode "_"
     1.8 -          (NameSpace.qualified qualifier "induct" :: vs' @ Ps @
     1.9 -             ["correctness"]), thm), []) thy;
    1.10 +        val (thm', thy') = PureThy.store_thm (space_implode "_"
    1.11 +          (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"]), thm) thy;
    1.12          val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
    1.13            (DatatypeAux.split_conj_thm thm');
    1.14          val ([thms'], thy'') = PureThy.add_thmss
    1.15 @@ -457,8 +456,8 @@
    1.16             rewrite_goals_tac rews,
    1.17             REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
    1.18               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
    1.19 -        val (thm', thy') = PureThy.store_thm ((space_implode "_"
    1.20 -          (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
    1.21 +        val (thm', thy') = PureThy.store_thm (space_implode "_"
    1.22 +          (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm) thy
    1.23        in
    1.24          Extraction.add_realizers_i
    1.25            [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'