--- a/src/HOL/Tools/record.ML Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Tools/record.ML Sun Feb 07 19:33:34 2010 +0100
@@ -1014,7 +1014,7 @@
else if Goal.future_enabled () then
Goal.future_result (ProofContext.init thy) (Future.fork_pri ~1 prf) prop
else prf ()
- in Drule.standard thm end;
+ in Drule.export_without_context thm end;
fun prove_common immediate stndrd thy asms prop tac =
let
@@ -1023,7 +1023,7 @@
else if immediate orelse not (Goal.future_enabled ()) then Goal.prove
else Goal.prove_future;
val prf = prv (ProofContext.init thy) [] asms prop tac;
- in if stndrd then Drule.standard prf else prf end;
+ in if stndrd then Drule.export_without_context prf else prf end;
val prove_future_global = prove_common false;
val prove_global = prove_common true;
@@ -1072,7 +1072,7 @@
if is_sel_upd_pair thy acc upd
then o_eq_dest
else o_eq_id_dest;
- in Drule.standard (othm RS dest) end;
+ in Drule.export_without_context (othm RS dest) end;
in map get_simp upd_funs end;
fun get_updupd_simp thy defset u u' comp =
@@ -1092,7 +1092,7 @@
REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
TRY (simp_tac (HOL_ss addsimps [id_apply]) 1));
val dest = if comp then o_eq_dest_lhs else o_eq_dest;
- in Drule.standard (othm RS dest) end;
+ in Drule.export_without_context (othm RS dest) end;
fun get_updupd_simps thy term defset =
let
@@ -1279,8 +1279,8 @@
val ss = get_sel_upd_defs thy;
val uathm = get_upd_acc_cong_thm upd acc thy ss;
in
- [Drule.standard (uathm RS updacc_noopE),
- Drule.standard (uathm RS updacc_noop_compE)]
+ [Drule.export_without_context (uathm RS updacc_noopE),
+ Drule.export_without_context (uathm RS updacc_noop_compE)]
end;
(*If f is constant then (f o g) = f. We know that K_skeleton
@@ -1721,8 +1721,8 @@
to prove other theorems. We haven't given names to the accessors
f, g etc yet however, so we generate an ext structure with
free variables as all arguments and allow the introduction tactic to
- operate on it as far as it can. We then use Drule.standard to convert
- the free variables into unifiable variables and unify them with
+ operate on it as far as it can. We then use Drule.export_without_context
+ to convert the free variables into unifiable variables and unify them with
(roughly) the definition of the accessor.*)
fun surject_prf () =
let
@@ -1733,7 +1733,7 @@
REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1;
val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
val [halfway] = Seq.list_of (tactic1 start);
- val [surject] = Seq.list_of (tactic2 (Drule.standard halfway));
+ val [surject] = Seq.list_of (tactic2 (Drule.export_without_context halfway));
in
surject
end;
@@ -2136,14 +2136,14 @@
fun sel_convs_prf () =
map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props;
val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
- fun sel_convs_standard_prf () = map Drule.standard sel_convs
+ fun sel_convs_standard_prf () = map Drule.export_without_context sel_convs;
val sel_convs_standard =
timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
fun upd_convs_prf () =
map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props;
val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
- fun upd_convs_standard_prf () = map Drule.standard upd_convs
+ fun upd_convs_standard_prf () = map Drule.export_without_context upd_convs;
val upd_convs_standard =
timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
@@ -2151,7 +2151,7 @@
let
val symdefs = map symmetric (sel_defs @ upd_defs);
val fold_ss = HOL_basic_ss addsimps symdefs;
- val ua_congs = map (Drule.standard o simplify fold_ss) upd_acc_cong_assists;
+ val ua_congs = map (Drule.export_without_context o simplify fold_ss) upd_acc_cong_assists;
in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
val (fold_congs, unfold_congs) =
timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
@@ -2221,7 +2221,7 @@
rtac (prop_subst OF [surjective]),
REPEAT o etac meta_allE, atac]);
val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
- fun split_meta_standardise () = Drule.standard split_meta;
+ fun split_meta_standardise () = Drule.export_without_context split_meta;
val split_meta_standard =
timeit_msg "record split_meta standard:" split_meta_standardise;