src/HOL/Tools/record.ML

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