simplified PureThy.store_thm;
authorwenzelm
Sat Mar 29 19:14:03 2008 +0100 (2008-03-29)
changeset 2648192e901171cc8
parent 26480 544cef16045b
child 26482 e7f677b85bfd
simplified PureThy.store_thm;
src/HOL/Import/hol4rews.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/specification_package.ML
src/Pure/Proof/extraction.ML
     1.1 --- a/src/HOL/Import/hol4rews.ML	Sat Mar 29 19:14:00 2008 +0100
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Sat Mar 29 19:14:03 2008 +0100
     1.3 @@ -390,7 +390,7 @@
     1.4          val thm2 = standard thm1;
     1.5        in
     1.6          thy
     1.7 -        |> PureThy.store_thm ((bthm, thm2), [])
     1.8 +        |> PureThy.store_thm (bthm, thm2)
     1.9          |> snd
    1.10          |> add_hol4_theorem bthy bthm hth
    1.11        end;
     2.1 --- a/src/HOL/Tools/datatype_realizer.ML	Sat Mar 29 19:14:00 2008 +0100
     2.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sat Mar 29 19:14:03 2008 +0100
     2.3 @@ -131,8 +131,7 @@
     2.4      val vs = map (fn i => List.nth (pnames, i)) is;
     2.5      val (thm', thy') = thy
     2.6        |> Sign.absolute_path
     2.7 -      |> PureThy.store_thm
     2.8 -        ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), [])
     2.9 +      |> PureThy.store_thm (space_implode "_" (ind_name :: vs @ ["correctness"]), thm)
    2.10        ||> Sign.restore_naming thy;
    2.11  
    2.12      val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
    2.13 @@ -198,7 +197,7 @@
    2.14      val exh_name = Thm.get_name exhaustion;
    2.15      val (thm', thy') = thy
    2.16        |> Sign.absolute_path
    2.17 -      |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), [])
    2.18 +      |> PureThy.store_thm (exh_name ^ "_P_correctness", thm)
    2.19        ||> Sign.restore_naming thy;
    2.20  
    2.21      val P = Var (("P", 0), rT' --> HOLogic.boolT);
     3.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Mar 29 19:14:00 2008 +0100
     3.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Mar 29 19:14:03 2008 +0100
     3.3 @@ -396,9 +396,8 @@
     3.4             REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
     3.5               [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
     3.6                DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
     3.7 -        val (thm', thy') = PureThy.store_thm ((space_implode "_"
     3.8 -          (NameSpace.qualified qualifier "induct" :: vs' @ Ps @
     3.9 -             ["correctness"]), thm), []) thy;
    3.10 +        val (thm', thy') = PureThy.store_thm (space_implode "_"
    3.11 +          (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"]), thm) thy;
    3.12          val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
    3.13            (DatatypeAux.split_conj_thm thm');
    3.14          val ([thms'], thy'') = PureThy.add_thmss
    3.15 @@ -457,8 +456,8 @@
    3.16             rewrite_goals_tac rews,
    3.17             REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
    3.18               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
    3.19 -        val (thm', thy') = PureThy.store_thm ((space_implode "_"
    3.20 -          (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
    3.21 +        val (thm', thy') = PureThy.store_thm (space_implode "_"
    3.22 +          (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm) thy
    3.23        in
    3.24          Extraction.add_realizers_i
    3.25            [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
     4.1 --- a/src/HOL/Tools/specification_package.ML	Sat Mar 29 19:14:00 2008 +0100
     4.2 +++ b/src/HOL/Tools/specification_package.ML	Sat Mar 29 19:14:03 2008 +0100
     4.3 @@ -185,7 +185,7 @@
     4.4                              if name = ""
     4.5                              then arg |> Library.swap
     4.6                              else (writeln ("  " ^ name ^ ": " ^ (string_of_thm thm));
     4.7 -                                  PureThy.store_thm ((name, thm), []) thy)
     4.8 +                                  PureThy.store_thm (name, thm) thy)
     4.9                      in
    4.10                          args |> apsnd (remove_alls frees)
    4.11                               |> apsnd undo_imps
     5.1 --- a/src/Pure/Proof/extraction.ML	Sat Mar 29 19:14:00 2008 +0100
     5.2 +++ b/src/Pure/Proof/extraction.ML	Sat Mar 29 19:14:03 2008 +0100
     5.3 @@ -735,11 +735,11 @@
     5.4                      Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
     5.5             in
     5.6               thy'
     5.7 -             |> PureThy.store_thm ((corr_name s vs,
     5.8 +             |> PureThy.store_thm (corr_name s vs,
     5.9                    Thm.varifyT (funpow (length (term_vars corr_prop))
    5.10                      (forall_elim_var 0) (forall_intr_frees
    5.11                        (ProofChecker.thm_of_proof thy'
    5.12 -                       (fst (Proofterm.freeze_thaw_prf prf)))))), [])
    5.13 +                       (fst (Proofterm.freeze_thaw_prf prf))))))
    5.14               |> snd
    5.15               |> fold Code.add_default_func def_thms
    5.16             end