# HG changeset patch
# User wenzelm
# Date 1265567614 -3600
# Node ID c839a4c670c695df4c6e93c597f0dc6c4b71865d
# Parent  862a20ffa8e2dd23c973fe364dbb5be9b8251227
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;

diff -r 862a20ffa8e2 -r c839a4c670c6 NEWS
--- a/NEWS	Sun Feb 07 19:31:55 2010 +0100
+++ b/NEWS	Sun Feb 07 19:33:34 2010 +0100
@@ -60,6 +60,10 @@
 
 *** ML ***
 
+* Renamed old-style Drule.standard to Drule.export_without_context, to
+emphasize that this is in no way a standard operation.
+INCOMPATIBILITY.
+
 * Curried take and drop in library.ML; negative length is interpreted
 as infinity (as in chop).  INCOMPATIBILITY.
 
diff -r 862a20ffa8e2 -r c839a4c670c6 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/FOL/simpdata.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -27,9 +27,9 @@
 
 (*Congruence rules for = or <-> (instead of ==)*)
 fun mk_meta_cong rl =
-  Drule.standard (mk_meta_eq (mk_meta_prems rl))
-  handle THM _ =>
-  error("Premises and conclusion of congruence rules must use =-equality or <->");
+  Drule.export_without_context (mk_meta_eq (mk_meta_prems rl))
+    handle THM _ =>
+      error("Premises and conclusion of congruence rules must use =-equality or <->");
 
 val mksimps_pairs =
   [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),
diff -r 862a20ffa8e2 -r c839a4c670c6 src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/FOLP/simp.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -519,7 +519,7 @@
 (* Compute Congruence rules for individual constants using the substition
    rules *)
 
-val subst_thms = map Drule.standard subst_thms;
+val subst_thms = map Drule.export_without_context subst_thms;
 
 
 fun exp_app(0,t) = t
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Import/hol4rews.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -371,7 +371,7 @@
     fun process ((bthy,bthm), hth as (_,thm)) thy =
       let
         val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm);
-        val thm2 = Drule.standard thm1;
+        val thm2 = Drule.export_without_context thm1;
       in
         thy
         |> PureThy.store_thm (Binding.name bthm, thm2)
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Import/shuffler.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -100,7 +100,7 @@
         val th4 = implies_elim_list (assume cPPQ) [th3,th3]
                                     |> implies_intr_list [cPPQ,cP]
     in
-        equal_intr th4 th1 |> Drule.standard
+        equal_intr th4 th1 |> Drule.export_without_context
     end
 
 val imp_comm =
@@ -120,7 +120,7 @@
         val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP]
                                     |> implies_intr_list [cQPR,cP,cQ]
     in
-        equal_intr th1 th2 |> Drule.standard
+        equal_intr th1 th2 |> Drule.export_without_context
     end
 
 val def_norm =
@@ -147,7 +147,7 @@
                               |> forall_intr cv
                               |> implies_intr cPQ
     in
-        equal_intr th1 th2 |> Drule.standard
+        equal_intr th1 th2 |> Drule.export_without_context
     end
 
 val all_comm =
@@ -173,7 +173,7 @@
                          |> forall_intr_list [cy,cx]
                          |> implies_intr cl
     in
-        equal_intr th1 th2 |> Drule.standard
+        equal_intr th1 th2 |> Drule.export_without_context
     end
 
 val equiv_comm =
@@ -187,7 +187,7 @@
         val th1  = assume ctu |> symmetric |> implies_intr ctu
         val th2  = assume cut |> symmetric |> implies_intr cut
     in
-        equal_intr th1 th2 |> Drule.standard
+        equal_intr th1 th2 |> Drule.export_without_context
     end
 
 (* This simplification procedure rewrites !!x y. P x y
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOL/Matrix/cplex/matrixlp.ML
--- a/src/HOL/Matrix/cplex/matrixlp.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Matrix/cplex/matrixlp.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -18,7 +18,7 @@
 
 fun inst_real thm =
   let val certT = ctyp_of (Thm.theory_of_thm thm) in
-    Drule.standard (Thm.instantiate
+    Drule.export_without_context (Thm.instantiate
       ([(certT (TVar (hd (OldTerm.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
   end
 
@@ -59,7 +59,7 @@
         val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
         val v = TVar (hd (sort ord (OldTerm.term_tvars (prop_of thm))))
     in
-        Drule.standard (Thm.instantiate ([(certT v, certT ty)], []) thm)
+        Drule.export_without_context (Thm.instantiate ([(certT v, certT ty)], []) thm)
     end
 
 fun inst_tvars [] thms = thms
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -152,7 +152,7 @@
 
 fun projections rule =
   Project_Rule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
-  |> map (Drule.standard #> Rule_Cases.save rule);
+  |> map (Drule.export_without_context #> Rule_Cases.save rule);
 
 val supp_prod = thm "supp_prod";
 val fresh_prod = thm "fresh_prod";
@@ -312,7 +312,7 @@
 
     val unfolded_perm_eq_thms =
       if length descr = length new_type_names then []
-      else map Drule.standard (List.drop (split_conj_thm
+      else map Drule.export_without_context (List.drop (split_conj_thm
         (Goal.prove_global thy2 [] []
           (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
             (map (fn (c as (s, T), x) =>
@@ -332,7 +332,7 @@
 
     val perm_empty_thms = maps (fn a =>
       let val permT = mk_permT (Type (a, []))
-      in map Drule.standard (List.take (split_conj_thm
+      in map Drule.export_without_context (List.take (split_conj_thm
         (Goal.prove_global thy2 [] []
           (augment_sort thy2 [pt_class_of thy2 a]
             (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
@@ -364,7 +364,7 @@
         val pt_inst = pt_inst_of thy2 a;
         val pt2' = pt_inst RS pt2;
         val pt2_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
-      in List.take (map Drule.standard (split_conj_thm
+      in List.take (map Drule.export_without_context (split_conj_thm
         (Goal.prove_global thy2 [] []
            (augment_sort thy2 [pt_class_of thy2 a]
              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
@@ -399,7 +399,7 @@
         val pt3' = pt_inst RS pt3;
         val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
         val pt3_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
-      in List.take (map Drule.standard (split_conj_thm
+      in List.take (map Drule.export_without_context (split_conj_thm
         (Goal.prove_global thy2 [] []
           (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
              (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
@@ -586,7 +586,7 @@
       (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
       (perm_indnames ~~ descr);
 
-    fun mk_perm_closed name = map (fn th => Drule.standard (th RS mp))
+    fun mk_perm_closed name = map (fn th => Drule.export_without_context (th RS mp))
       (List.take (split_conj_thm (Goal.prove_global thy4 [] []
         (augment_sort thy4
           (pt_class_of thy4 name :: map (cp_class_of thy4 name) (remove (op =) name dt_atoms))
@@ -812,7 +812,8 @@
         val rep_const = cterm_of thy
           (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
         val dist =
-          Drule.standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
+          Drule.export_without_context
+            (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
         val (thy', defs', eqns') = fold (make_constr_def tname T T')
           (constrs ~~ constrs' ~~ constr_syntax) (Sign.add_path tname thy, defs, [])
       in
@@ -877,8 +878,9 @@
           let
             val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
               simp_tac (global_simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
-          in dist_thm :: Drule.standard (dist_thm RS not_sym) ::
-            prove_distinct_thms p (k, ts)
+          in
+            dist_thm :: Drule.export_without_context (dist_thm RS not_sym) ::
+              prove_distinct_thms p (k, ts)
           end;
 
     val distinct_thms = map2 prove_distinct_thms
@@ -1092,7 +1094,7 @@
 
     val finite_supp_thms = map (fn atom =>
       let val atomT = Type (atom, [])
-      in map Drule.standard (List.take
+      in map Drule.export_without_context (List.take
         (split_conj_thm (Goal.prove_global thy8 [] []
            (augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort)
              (HOLogic.mk_Trueprop
@@ -1540,7 +1542,7 @@
           in
             (R $ x $ y, R' $ mk_perm [] pi x $ mk_perm [] pi y)
           end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs));
-        val ths = map (fn th => Drule.standard (th RS mp)) (split_conj_thm
+        val ths = map (fn th => Drule.export_without_context (th RS mp)) (split_conj_thm
           (Goal.prove_global thy11 [] []
             (augment_sort thy1 pt_cp_sort
               (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
@@ -1572,7 +1574,7 @@
           (finite $ (Const ("Nominal.supp", T --> aset) $ f)))
             (rec_fns ~~ rec_fn_Ts)
       in
-        map (fn th => Drule.standard (th RS mp)) (split_conj_thm
+        map (fn th => Drule.export_without_context (th RS mp)) (split_conj_thm
           (Goal.prove_global thy11 []
             (map (augment_sort thy11 fs_cp_sort) fins)
             (augment_sort thy11 fs_cp_sort
@@ -1615,7 +1617,7 @@
             val y = Free ("y", U);
             val y' = Free ("y'", U)
           in
-            Drule.standard (Goal.prove (ProofContext.init thy11) []
+            Drule.export_without_context (Goal.prove (ProofContext.init thy11) []
               (map (augment_sort thy11 fs_cp_sort)
                 (finite_prems @
                    [HOLogic.mk_Trueprop (R $ x $ y),
@@ -2060,7 +2062,7 @@
          ((Binding.name "rec_equiv'", flat rec_equiv_thms'), []),
          ((Binding.name "rec_fin_supp", flat rec_fin_supp_thms), []),
          ((Binding.name "rec_fresh", flat rec_fresh_thms), []),
-         ((Binding.name "rec_unique", map Drule.standard rec_unique_thms), []),
+         ((Binding.name "rec_unique", map Drule.export_without_context rec_unique_thms), []),
          ((Binding.name "recs", rec_thms), [])] ||>
       Sign.parent_path ||>
       map_nominal_datatypes (fold Symtab.update dt_infos);
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -310,7 +310,7 @@
                   val prop = list_all ([("n",nT),("x",eT)],
                               Logic.mk_equals (Const ("Ex",Tex)$Abs(s,T,eq),
                                                HOLogic.true_const));
-                  val thm = Drule.standard (prove prop);
+                  val thm = Drule.export_without_context (prove prop);
                   val thm' = if swap then swap_ex_eq OF [thm] else thm
              in SOME thm' end
              handle TERM _ => NONE)
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -253,9 +253,11 @@
         val rep_const = cterm_of thy
           (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> Univ_elT));
         val cong' =
-          Drule.standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
+          Drule.export_without_context
+            (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
         val dist =
-          Drule.standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
+          Drule.export_without_context
+            (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
         val (thy', defs', eqns', _) = fold ((make_constr_def tname T) (length constrs))
           (constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1);
       in
@@ -532,7 +534,7 @@
               let
                 val dist_thm = Skip_Proof.prove_global thy5 [] [] t (fn _ =>
                   EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
-              in dist_thm :: Drule.standard (dist_thm RS not_sym) :: prove ts end;
+              in dist_thm :: Drule.export_without_context (dist_thm RS not_sym) :: prove ts end;
       in prove ts end;
 
     val distinct_thms = map2 (prove_distinct_thms)
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -197,7 +197,7 @@
 
     fun prove_size_eqs p size_fns size_ofp simpset =
       maps (fn (((_, (_, _, constrs)), size_const), T) =>
-        map (fn constr => Drule.standard (Skip_Proof.prove ctxt [] []
+        map (fn constr => Drule.export_without_context (Skip_Proof.prove ctxt [] []
           (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
              size_ofp size_const T constr)
           (fn _ => simp_tac simpset 1))) constrs)
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -577,7 +577,7 @@
         (*val elim = singleton (Inductive_Set.codegen_preproc thy) (preprocess_elim thy nparams 
           (expand_tuples_elim pre_elim))*)
         val elim =
-          (Drule.standard o Skip_Proof.make_thm thy)
+          (Drule.export_without_context o Skip_Proof.make_thm thy)
           (mk_casesrule (ProofContext.init thy) pred intros)
       in
         mk_pred_data ((intros, SOME elim), no_compilation)
@@ -641,7 +641,7 @@
       else ()
     val pred = Const (constname, T)
     val pre_elim = 
-      (Drule.standard o Skip_Proof.make_thm thy)
+      (Drule.export_without_context o Skip_Proof.make_thm thy)
       (mk_casesrule (ProofContext.init thy) pred pre_intros)
   in register_predicate (constname, pre_intros, pre_elim) thy end
 
@@ -2178,7 +2178,8 @@
     (join_preds_modes moded_clauses compiled_terms)
 
 fun prove_by_skip options thy _ _ _ _ compiled_terms =
-  map_preds_modes (fn pred => fn mode => fn t => Drule.standard (Skip_Proof.make_thm thy t))
+  map_preds_modes
+    (fn pred => fn mode => fn t => Drule.export_without_context (Skip_Proof.make_thm thy t))
     compiled_terms
 
 (* preparation of introduction rules into special datastructures *)
@@ -2269,7 +2270,7 @@
         val elim = the_elim_of thy predname
         val nparams = nparams_of thy predname
         val elim' =
-          (Drule.standard o (Skip_Proof.make_thm thy))
+          (Drule.export_without_context o Skip_Proof.make_thm thy)
           (mk_casesrule (ProofContext.init thy) nparams intros)
       in
         if not (Thm.equiv_thm (elim, elim')) then
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -391,7 +391,7 @@
         |> map (fn (concl'::conclprems, _) =>
           Logic.list_implies ((flat prems') @ conclprems, concl')))
   in
-    map (Drule.standard o (Skip_Proof.make_thm thy)) intro_ts'
+    map (Drule.export_without_context o Skip_Proof.make_thm thy) intro_ts'
   end
 
 end;
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -129,7 +129,7 @@
 
 (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
 val meta_outer =
-  curry_rule o Drule.standard o
+  curry_rule o Drule.export_without_context o
   rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
 
 (*Strip off the outer !P*)
@@ -151,7 +151,7 @@
                {f = f, R = R, rules = rules,
                 full_pats_TCs = full_pats_TCs,
                 TCs = TCs}
-       val rules' = map (Drule.standard o ObjectLogic.rulify_no_asm)
+       val rules' = map (Drule.export_without_context o ObjectLogic.rulify_no_asm)
                         (R.CONJUNCTS rules)
          in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
         rules = ListPair.zip(rules', rows),
@@ -180,7 +180,7 @@
     | solve_eq (th, [a], i) = [(a, i)]
     | solve_eq (th, splitths as (_ :: _), i) = 
       (writeln "Proving unsplit equation...";
-      [((Drule.standard o ObjectLogic.rulify_no_asm)
+      [((Drule.export_without_context o ObjectLogic.rulify_no_asm)
           (CaseSplit.splitto splitths th), i)])
       (* if there's an error, pretend nothing happened with this definition 
          We should probably print something out so that the user knows...? *)
@@ -236,7 +236,7 @@
  in (theory,
      (*return the conjoined induction rule and recursion equations,
        with assumptions remaining to discharge*)
-     Drule.standard (induction RS (rules RS conjI)))
+     Drule.export_without_context (induction RS (rules RS conjI)))
  end
 
 fun defer thy congs fid seqs =
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Tools/arith_data.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -110,8 +110,8 @@
 
 fun prove_conv tacs ctxt (_: thm list) = prove_conv_nohyps tacs ctxt;
 
-fun prove_conv2 expand_tac norm_tac ss tu = (*FIXME avoid standard*)
-  mk_meta_eq (Drule.standard (Goal.prove (Simplifier.the_context ss) [] []
+fun prove_conv2 expand_tac norm_tac ss tu = (* FIXME avoid Drule.export_without_context *)
+  mk_meta_eq (Drule.export_without_context (Goal.prove (Simplifier.the_context ss) [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
     (K (EVERY [expand_tac, norm_tac ss]))));
 
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -75,7 +75,7 @@
 fun add_specification axiomatic cos arg =
     arg |> apsnd Thm.freezeT
         |> proc_exprop axiomatic cos
-        |> apsnd Drule.standard
+        |> apsnd Drule.export_without_context
 
 
 (* Collect all intances of constants in term *)
@@ -189,7 +189,7 @@
                     in
                         args |> apsnd (remove_alls frees)
                              |> apsnd undo_imps
-                             |> apsnd Drule.standard
+                             |> apsnd Drule.export_without_context
                              |> Thm.theory_attributes (map (Attrib.attribute thy) atts)
                              |> add_final
                              |> Library.swap
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -544,7 +544,7 @@
       (fn NONE => "X" | SOME k' => string_of_int k')
         (ks @ [SOME k]))) arities));
 
-fun prep_intrs intrs = map (rename_term o #prop o rep_thm o Drule.standard) intrs;
+fun prep_intrs intrs = map (rename_term o #prop o rep_thm o Drule.export_without_context) intrs;
 
 fun constrain cs [] = []
   | constrain cs ((s, xs) :: ys) =
diff -r 862a20ffa8e2 -r c839a4c670c6 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;
 
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Tools/split_rule.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -100,13 +100,13 @@
       | (t, ts) => fold collect_vars ts);
 
 
-val split_rule_var = (Drule.standard o remove_internal_split) oo split_rule_var';
+val split_rule_var = (Drule.export_without_context o remove_internal_split) oo split_rule_var';
 
 (*curries ALL function variables occurring in a rule's conclusion*)
 fun split_rule rl =
   fold_rev split_rule_var' (OldTerm.term_vars (concl_of rl)) rl
   |> remove_internal_split
-  |> Drule.standard;
+  |> Drule.export_without_context;
 
 (*curries ALL function variables*)
 fun complete_split_rule rl =
@@ -117,7 +117,7 @@
   in
     fst (fold_rev complete_split_rule_var vars (rl, xs))
     |> remove_internal_split
-    |> Drule.standard
+    |> Drule.export_without_context
     |> Rule_Cases.save rl
   end;
 
@@ -137,7 +137,7 @@
     rl
     |> fold_index one_goal xss
     |> Simplifier.full_simplify split_rule_ss
-    |> Drule.standard
+    |> Drule.export_without_context
     |> Rule_Cases.save rl
   end;
 
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Tools/typedef.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -122,7 +122,7 @@
           let
             val cert = Thm.cterm_of (Thm.theory_of_thm def_eq);
             val goal_eq = MetaSimplifier.rewrite true [def_eq] (cert goal');
-          in Drule.standard (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
+          in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
 
     fun typedef_result inhabited =
       ObjectLogic.typedecl (t, vs, mx)
@@ -139,7 +139,7 @@
       ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps
       #-> (fn ([type_definition], set_def) => fn thy1 =>
         let
-          fun make th = Drule.standard (th OF [type_definition]);
+          fun make th = Drule.export_without_context (th OF [type_definition]);
           val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
               Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) =
             thy1
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -251,7 +251,7 @@
 
     (* register unfold theorems *)
     val (unfold_thms, thy) =
-      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard))
+      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context))
         (mk_unfold_thms unfold_binds tuple_unfold_thm) thy;
   in
     ((proj_thms, unfold_thms), thy)
@@ -446,7 +446,7 @@
     (* prove isomorphism and isodefl rules *)
     fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy =
       let
-        fun make thm = Drule.standard (thm OF [REP_eq, abs_def, rep_def]);
+        fun make thm = Drule.export_without_context (thm OF [REP_eq, abs_def, rep_def]);
         val rep_iso_thm = make @{thm domain_rep_iso};
         val abs_iso_thm = make @{thm domain_abs_iso};
         val isodefl_thm = make @{thm isodefl_abs_rep};
@@ -545,7 +545,7 @@
           val thmR = thm RS @{thm conjunct2};
         in (n, thmL):: conjuncts ns thmR end;
     val (isodefl_thms, thy) = thy |>
-      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard))
+      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context))
         (conjuncts isodefl_binds isodefl_thm);
     val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy;
 
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -180,7 +180,7 @@
 val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
 val abs_defin' = iso_locale RS iso_abs_defin';
 val rep_defin' = iso_locale RS iso_rep_defin';
-val iso_rews = map Drule.standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
+val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
 
 (* ----- generating beta reduction rules from definitions-------------------- *)
 
@@ -263,7 +263,7 @@
   val exhaust = pg con_appls (mk_trp exh) (K tacs);
   val _ = trace " Proving casedist...";
   val casedist =
-    Drule.standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
+    Drule.export_without_context (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
 end;
 
 local 
@@ -554,7 +554,7 @@
         flat
           (ListPair.map (distinct c) ((map #1 cs),leqs)) @
         distincts cs;
-  in map Drule.standard (distincts (cons ~~ distincts_le)) end;
+  in map Drule.export_without_context (distincts (cons ~~ distincts_le)) end;
 
 local 
   fun pgterm rel con args =
@@ -755,7 +755,7 @@
         maps (eq_tacs ctxt) eqs;
     in pg copy_take_defs goal tacs end;
 in
-  val take_rews = map Drule.standard
+  val take_rews = map Drule.export_without_context
     (atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps);
 end; (* local *)
 
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -89,7 +89,7 @@
           (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
     (* transfer thms so that they will know about the new cpo instance *)
     val cpo_thms' = map (Thm.transfer thy2) cpo_thms;
-    fun make thm = Drule.standard (thm OF cpo_thms');
+    fun make thm = Drule.export_without_context (thm OF cpo_thms');
     val ([adm, cont_Rep, cont_Abs, lub, thelub, compact], thy3) =
       thy2
       |> Sign.add_path (Binding.name_of name)
@@ -127,7 +127,7 @@
       |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
         (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
     val pcpo_thms' = map (Thm.transfer thy2) pcpo_thms;
-    fun make thm = Drule.standard (thm OF pcpo_thms');
+    fun make thm = Drule.export_without_context (thm OF pcpo_thms');
     val ([Rep_strict, Abs_strict, Rep_strict_iff, Abs_strict_iff,
           Rep_defined, Abs_defined], thy3) =
       thy2
diff -r 862a20ffa8e2 -r c839a4c670c6 src/HOLCF/Tools/repdef.ML
--- a/src/HOLCF/Tools/repdef.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOLCF/Tools/repdef.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -139,7 +139,7 @@
       |> Sign.add_path (Binding.name_of name)
       |> PureThy.add_thms
         [((Binding.prefix_name "REP_" name,
-          Drule.standard (@{thm typedef_REP} OF typedef_thms')), [])]
+          Drule.export_without_context (@{thm typedef_REP} OF typedef_thms')), [])]
       ||> Sign.parent_path;
 
     val rep_info =
diff -r 862a20ffa8e2 -r c839a4c670c6 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Provers/hypsubst.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -165,7 +165,7 @@
 
 end;
 
-val ssubst = Drule.standard (Data.sym RS Data.subst);
+val ssubst = Drule.export_without_context (Data.sym RS Data.subst);
 
 fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
   case try (Logic.strip_assums_hyp #> hd #>
diff -r 862a20ffa8e2 -r c839a4c670c6 src/Provers/typedsimp.ML
--- a/src/Provers/typedsimp.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Provers/typedsimp.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -43,11 +43,11 @@
 (*For simplifying both sides of an equation:
       [| a=c; b=c |] ==> b=a
   Can use resolve_tac [split_eqn] to prepare an equation for simplification. *)
-val split_eqn = Drule.standard (sym RSN (2,trans) RS sym);
+val split_eqn = Drule.export_without_context (sym RSN (2,trans) RS sym);
 
 
 (*    [| a=b; b=c |] ==> reduce(a,c)  *)
-val red_trans = Drule.standard (trans RS red_if_equal);
+val red_trans = Drule.export_without_context (trans RS red_if_equal);
 
 (*For REWRITE rule: Make a reduction rule for simplification, e.g.
   [| a: C(0); ... ; a=c: C(0) |] ==> rec(0,a,b) = c: C(0) *)
diff -r 862a20ffa8e2 -r c839a4c670c6 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Pure/Isar/attrib.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -298,7 +298,7 @@
   setup (Binding.name "params")
     (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
     "named rule parameters" #>
-  setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.standard)))
+  setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.export_without_context)))
     "result put into standard form (legacy)" #>
   setup (Binding.name "rule_format") rule_format "result put into canonical rule format" #>
   setup (Binding.name "elim_format") (Scan.succeed elim_format)
diff -r 862a20ffa8e2 -r c839a4c670c6 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Pure/Isar/class.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -86,7 +86,7 @@
       | SOME prop => Logic.mk_implies (Morphism.term const_morph
           ((map_types o map_atyps) (K aT) prop), of_class_prop_concl);
     val sup_of_classes = map (snd o rules thy) sups;
-    val loc_axiom_intros = map Drule.standard' (Locale.axioms_of thy class);
+    val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
     val axclass_intro = #intro (AxClass.get_info thy class);
     val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
     val tac = REPEAT (SOMEGOAL
diff -r 862a20ffa8e2 -r c839a4c670c6 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Pure/Isar/class_target.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -233,7 +233,7 @@
 fun register_subclass (sub, sup) some_dep_morph some_wit export thy =
   let
     val intros = (snd o rules thy) sup :: map_filter I
-      [Option.map (Drule.standard' o Element.conclude_witness) some_wit,
+      [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit,
         (fst o rules thy) sub];
     val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
     val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
diff -r 862a20ffa8e2 -r c839a4c670c6 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Pure/Isar/expression.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -699,7 +699,7 @@
             |> PureThy.note_thmss ""
                  [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
                   ((Binding.conceal (Binding.name axiomsN), []),
-                    [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
+                    [(map (Drule.export_without_context o Element.conclude_witness) axioms, [])])]
             ||> Sign.restore_naming thy''';
         in (SOME statement, SOME intro, axioms, thy'''') end;
   in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;
diff -r 862a20ffa8e2 -r c839a4c670c6 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Pure/Isar/skip_proof.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -39,6 +39,6 @@
       else tac args st);
 
 fun prove_global thy xs asms prop tac =
-  Drule.standard (prove (ProofContext.init thy) xs asms prop tac);
+  Drule.export_without_context (prove (ProofContext.init thy) xs asms prop tac);
 
 end;
diff -r 862a20ffa8e2 -r c839a4c670c6 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Pure/ML/ml_context.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -70,8 +70,8 @@
 val ml_store_thms = ml_store "";
 fun ml_store_thm (name, th) = ml_store "hd" (name, [th]);
 
-fun bind_thm (name, thm) = ml_store_thm (name, Drule.standard thm);
-fun bind_thms (name, thms) = ml_store_thms (name, map Drule.standard thms);
+fun bind_thm (name, thm) = ml_store_thm (name, Drule.export_without_context thm);
+fun bind_thms (name, thms) = ml_store_thms (name, map Drule.export_without_context thms);
 
 fun thm name = ProofContext.get_thm (the_local_context ()) name;
 fun thms name = ProofContext.get_thms (the_local_context ()) name;
diff -r 862a20ffa8e2 -r c839a4c670c6 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Pure/axclass.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -484,10 +484,10 @@
       def_thy
       |> Sign.mandatory_path (Binding.name_of bconst)
       |> PureThy.note_thmss ""
-        [((Binding.name introN, []), [([Drule.standard raw_intro], [])]),
-         ((Binding.name superN, []), [(map Drule.standard raw_classrel, [])]),
+        [((Binding.name introN, []), [([Drule.export_without_context raw_intro], [])]),
+         ((Binding.name superN, []), [(map Drule.export_without_context raw_classrel, [])]),
          ((Binding.name axiomsN, []),
-           [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
+           [(map (fn th => Drule.export_without_context (class_triv RS th)) raw_axioms, [])])]
       ||> Sign.restore_naming def_thy;
 
 
diff -r 862a20ffa8e2 -r c839a4c670c6 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Pure/drule.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -75,8 +75,8 @@
   val beta_conv: cterm -> cterm -> cterm
   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
   val flexflex_unique: thm -> thm
-  val standard: thm -> thm
-  val standard': thm -> thm
+  val export_without_context: thm -> thm
+  val export_without_context_open: thm -> thm
   val get_def: theory -> xstring -> thm
   val store_thm: binding -> thm -> thm
   val store_standard_thm: binding -> thm -> thm
@@ -303,9 +303,9 @@
     |  _   => raise THM("flexflex_unique: multiple unifiers", 0, [th]);
 
 
-(* legacy standard operations *)
+(* old-style export without context *)
 
-val standard' =
+val export_without_context_open =
   implies_intr_hyps
   #> forall_intr_frees
   #> `Thm.maxidx_of
@@ -315,9 +315,9 @@
     #> zero_var_indexes
     #> Thm.varifyT);
 
-val standard =
+val export_without_context =
   flexflex_unique
-  #> standard'
+  #> export_without_context_open
   #> Thm.close_derivation;
 
 
@@ -459,8 +459,8 @@
 fun store_thm_open name th =
   Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th)));
 
-fun store_standard_thm name th = store_thm name (standard th);
-fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
+fun store_standard_thm name th = store_thm name (export_without_context th);
+fun store_standard_thm_open name thm = store_thm_open name (export_without_context_open thm);
 
 val reflexive_thm =
   let val cx = certify (Var(("x",0),TVar(("'a",0),[])))
@@ -708,12 +708,12 @@
 val protect = Thm.capply (certify Logic.protectC);
 
 val protectI =
-  store_thm (Binding.conceal (Binding.name "protectI"))
-    (standard (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)));
+  store_standard_thm (Binding.conceal (Binding.name "protectI"))
+    (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A));
 
 val protectD =
-  store_thm (Binding.conceal (Binding.name "protectD"))
-    (standard (Thm.equal_elim prop_def (Thm.assume (protect A))));
+  store_standard_thm (Binding.conceal (Binding.name "protectD"))
+    (Thm.equal_elim prop_def (Thm.assume (protect A)));
 
 val protect_cong =
   store_standard_thm_open (Binding.name "protect_cong") (Thm.reflexive (protect A));
@@ -730,8 +730,8 @@
 (* term *)
 
 val termI =
-  store_thm (Binding.conceal (Binding.name "termI"))
-    (standard (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))));
+  store_standard_thm (Binding.conceal (Binding.name "termI"))
+    (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)));
 
 fun mk_term ct =
   let
@@ -759,15 +759,14 @@
 (* sort_constraint *)
 
 val sort_constraintI =
-  store_thm (Binding.conceal (Binding.name "sort_constraintI"))
-    (standard (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T)));
+  store_standard_thm (Binding.conceal (Binding.name "sort_constraintI"))
+    (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T));
 
 val sort_constraint_eq =
-  store_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
-    (standard
-      (Thm.equal_intr
-        (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
-        (implies_intr_list [A, C] (Thm.assume A))));
+  store_standard_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
+    (Thm.equal_intr
+      (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
+      (implies_intr_list [A, C] (Thm.assume A)));
 
 end;
 
@@ -983,5 +982,5 @@
 
 end;
 
-structure BasicDrule: BASIC_DRULE = Drule;
-open BasicDrule;
+structure Basic_Drule: BASIC_DRULE = Drule;
+open Basic_Drule;
diff -r 862a20ffa8e2 -r c839a4c670c6 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Pure/goal.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -210,7 +210,7 @@
 fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
 
 fun prove_global thy xs asms prop tac =
-  Drule.standard (prove (ProofContext.init thy) xs asms prop tac);
+  Drule.export_without_context (prove (ProofContext.init thy) xs asms prop tac);
 
 
 
diff -r 862a20ffa8e2 -r c839a4c670c6 src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Pure/old_goals.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -305,7 +305,7 @@
             val th = Goal.conclude ath
             val thy' = Thm.theory_of_thm th
             val {hyps, prop, ...} = Thm.rep_thm th
-            val final_th = Drule.standard th
+            val final_th = Drule.export_without_context th
         in  if not check then final_th
             else if not (Theory.eq_thy(thy,thy')) then !result_error_fn state
                 ("Theory of proof state has changed!" ^
@@ -512,7 +512,7 @@
             0 => thm
           | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
   in
-    Drule.standard (implies_intr_list As
+    Drule.export_without_context (implies_intr_list As
       (check (Seq.pull (EVERY (f asms) (trivial B)))))
   end;
 
diff -r 862a20ffa8e2 -r c839a4c670c6 src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Sequents/simpdata.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -49,9 +49,9 @@
 
 (*Congruence rules for = or <-> (instead of ==)*)
 fun mk_meta_cong rl =
-  Drule.standard(mk_meta_eq (mk_meta_prems rl))
-  handle THM _ =>
-  error("Premises and conclusion of congruence rules must use =-equality or <->");
+  Drule.export_without_context(mk_meta_eq (mk_meta_prems rl))
+    handle THM _ =>
+      error("Premises and conclusion of congruence rules must use =-equality or <->");
 
 
 (*** Standard simpsets ***)
diff -r 862a20ffa8e2 -r c839a4c670c6 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -292,7 +292,7 @@
          rtac case_trans 1,
          REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]);
 
-  val free_iffs = map Drule.standard (con_defs RL [@{thm def_swap_iff}]);
+  val free_iffs = map Drule.export_without_context (con_defs RL [@{thm def_swap_iff}]);
 
   val case_eqns = map prove_case_eqn (flat con_ty_lists ~~ case_args ~~ tl con_defs);
 
@@ -338,7 +338,7 @@
   val constructors =
       map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
 
-  val free_SEs = map Drule.standard (Ind_Syntax.mk_free_SEs free_iffs);
+  val free_SEs = map Drule.export_without_context (Ind_Syntax.mk_free_SEs free_iffs);
 
   val {intrs, elim, induct, mutual_induct, ...} = ind_result
 
diff -r 862a20ffa8e2 -r c839a4c670c6 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -193,9 +193,9 @@
         [rtac (@{thm Collect_subset} RS @{thm bnd_monoI}) 1,
          REPEAT (ares_tac (@{thms basic_monos} @ monos) 1)]);
 
-  val dom_subset = Drule.standard (big_rec_def RS Fp.subs);
+  val dom_subset = Drule.export_without_context (big_rec_def RS Fp.subs);
 
-  val unfold = Drule.standard ([big_rec_def, bnd_mono] MRS Fp.Tarski);
+  val unfold = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.Tarski);
 
   (********)
   val dummy = writeln "  Proving the introduction rules...";
@@ -205,7 +205,7 @@
   val Part_trans =
       case rec_names of
            [_] => asm_rl
-         | _   => Drule.standard (@{thm Part_subset} RS @{thm subset_trans});
+         | _   => Drule.export_without_context (@{thm Part_subset} RS @{thm subset_trans});
 
   (*To type-check recursive occurrences of the inductive sets, possibly
     enclosed in some monotonic operator M.*)
@@ -272,7 +272,7 @@
     rule_by_tactic
       (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac ss) THEN basic_elim_tac)
       (Thm.assume A RS elim)
-      |> Drule.standard';
+      |> Drule.export_without_context_open;
 
   fun induction_rules raw_induct thy =
    let
@@ -503,7 +503,7 @@
      val Const (@{const_name Trueprop}, _) $ (pred_var $ _) = concl_of induct0
 
      val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0)
-                  |> Drule.standard
+                  |> Drule.export_without_context
      and mutual_induct = CP.remove_split mutual_induct_fsplit
 
      val ([induct', mutual_induct'], thy') =
@@ -514,7 +514,7 @@
     in ((thy', induct'), mutual_induct')
     end;  (*of induction_rules*)
 
-  val raw_induct = Drule.standard ([big_rec_def, bnd_mono] MRS Fp.induct)
+  val raw_induct = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.induct)
 
   val ((thy2, induct), mutual_induct) =
     if not coind then induction_rules raw_induct thy1
diff -r 862a20ffa8e2 -r c839a4c670c6 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/ZF/ind_syntax.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -114,7 +114,7 @@
   | tryres (th, []) = raise THM("tryres", 0, [th]);
 
 fun gen_make_elim elim_rls rl =
-      Drule.standard (tryres (rl, elim_rls @ [revcut_rl]));
+  Drule.export_without_context (tryres (rl, elim_rls @ [revcut_rl]));
 
 (*Turns iff rules into safe elimination rules*)
 fun mk_free_SEs iffs = map (gen_make_elim [@{thm conjE}, @{thm FalseE}]) (iffs RL [@{thm iffD1}]);