--- 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;
--- 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);
--- 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'
--- 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
--- 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