# HG changeset patch
# User wenzelm
# Date 1206814443 -3600
# Node ID 92e901171cc85344cce15b3017a37430a6cec759
# Parent  544cef16045b712b4d8664d9d8e747a9d4a03d4a
simplified PureThy.store_thm;

diff -r 544cef16045b -r 92e901171cc8 src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Sat Mar 29 19:14:00 2008 +0100
+++ b/src/HOL/Import/hol4rews.ML	Sat Mar 29 19:14:03 2008 +0100
@@ -390,7 +390,7 @@
         val thm2 = standard thm1;
       in
         thy
-        |> PureThy.store_thm ((bthm, thm2), [])
+        |> PureThy.store_thm (bthm, thm2)
         |> snd
         |> add_hol4_theorem bthy bthm hth
       end;
diff -r 544cef16045b -r 92e901171cc8 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Sat Mar 29 19:14:00 2008 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Sat Mar 29 19:14:03 2008 +0100
@@ -131,8 +131,7 @@
     val vs = map (fn i => List.nth (pnames, i)) is;
     val (thm', thy') = thy
       |> Sign.absolute_path
-      |> PureThy.store_thm
-        ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), [])
+      |> PureThy.store_thm (space_implode "_" (ind_name :: vs @ ["correctness"]), thm)
       ||> Sign.restore_naming thy;
 
     val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
@@ -198,7 +197,7 @@
     val exh_name = Thm.get_name exhaustion;
     val (thm', thy') = thy
       |> Sign.absolute_path
-      |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), [])
+      |> PureThy.store_thm (exh_name ^ "_P_correctness", thm)
       ||> Sign.restore_naming thy;
 
     val P = Var (("P", 0), rT' --> HOLogic.boolT);
diff -r 544cef16045b -r 92e901171cc8 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Sat Mar 29 19:14:00 2008 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sat Mar 29 19:14:03 2008 +0100
@@ -396,9 +396,8 @@
            REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
              [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 @
-             ["correctness"]), thm), []) thy;
+        val (thm', thy') = PureThy.store_thm (space_implode "_"
+          (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"]), thm) thy;
         val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
           (DatatypeAux.split_conj_thm thm');
         val ([thms'], thy'') = PureThy.add_thmss
@@ -457,8 +456,8 @@
            rewrite_goals_tac rews,
            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
+        val (thm', thy') = PureThy.store_thm (space_implode "_"
+          (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm) thy
       in
         Extraction.add_realizers_i
           [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
diff -r 544cef16045b -r 92e901171cc8 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Sat Mar 29 19:14:00 2008 +0100
+++ b/src/HOL/Tools/specification_package.ML	Sat Mar 29 19:14:03 2008 +0100
@@ -185,7 +185,7 @@
                             if name = ""
                             then arg |> Library.swap
                             else (writeln ("  " ^ name ^ ": " ^ (string_of_thm thm));
-                                  PureThy.store_thm ((name, thm), []) thy)
+                                  PureThy.store_thm (name, thm) thy)
                     in
                         args |> apsnd (remove_alls frees)
                              |> apsnd undo_imps
diff -r 544cef16045b -r 92e901171cc8 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sat Mar 29 19:14:00 2008 +0100
+++ b/src/Pure/Proof/extraction.ML	Sat Mar 29 19:14:03 2008 +0100
@@ -735,11 +735,11 @@
                     Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
            in
              thy'
-             |> PureThy.store_thm ((corr_name s vs,
+             |> PureThy.store_thm (corr_name s vs,
                   Thm.varifyT (funpow (length (term_vars corr_prop))
                     (forall_elim_var 0) (forall_intr_frees
                       (ProofChecker.thm_of_proof thy'
-                       (fst (Proofterm.freeze_thaw_prf prf)))))), [])
+                       (fst (Proofterm.freeze_thaw_prf prf))))))
              |> snd
              |> fold Code.add_default_func def_thms
            end