renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
authorwenzelm
Sun Feb 07 19:33:34 2010 +0100 (2010-02-07)
changeset 35021c839a4c670c6
parent 35020 862a20ffa8e2
child 35022 c844b93dd147
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
NEWS
src/FOL/simpdata.ML
src/FOLP/simp.ML
src/HOL/Import/hol4rews.ML
src/HOL/Import/shuffler.ML
src/HOL/Matrix/cplex/matrixlp.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/record.ML
src/HOL/Tools/split_rule.ML
src/HOL/Tools/typedef.ML
src/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
src/HOLCF/Tools/pcpodef.ML
src/HOLCF/Tools/repdef.ML
src/Provers/hypsubst.ML
src/Provers/typedsimp.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/class.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/skip_proof.ML
src/Pure/ML/ml_context.ML
src/Pure/axclass.ML
src/Pure/drule.ML
src/Pure/goal.ML
src/Pure/old_goals.ML
src/Sequents/simpdata.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
src/ZF/ind_syntax.ML
     1.1 --- a/NEWS	Sun Feb 07 19:31:55 2010 +0100
     1.2 +++ b/NEWS	Sun Feb 07 19:33:34 2010 +0100
     1.3 @@ -60,6 +60,10 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Renamed old-style Drule.standard to Drule.export_without_context, to
     1.8 +emphasize that this is in no way a standard operation.
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  * Curried take and drop in library.ML; negative length is interpreted
    1.12  as infinity (as in chop).  INCOMPATIBILITY.
    1.13  
     2.1 --- a/src/FOL/simpdata.ML	Sun Feb 07 19:31:55 2010 +0100
     2.2 +++ b/src/FOL/simpdata.ML	Sun Feb 07 19:33:34 2010 +0100
     2.3 @@ -27,9 +27,9 @@
     2.4  
     2.5  (*Congruence rules for = or <-> (instead of ==)*)
     2.6  fun mk_meta_cong rl =
     2.7 -  Drule.standard (mk_meta_eq (mk_meta_prems rl))
     2.8 -  handle THM _ =>
     2.9 -  error("Premises and conclusion of congruence rules must use =-equality or <->");
    2.10 +  Drule.export_without_context (mk_meta_eq (mk_meta_prems rl))
    2.11 +    handle THM _ =>
    2.12 +      error("Premises and conclusion of congruence rules must use =-equality or <->");
    2.13  
    2.14  val mksimps_pairs =
    2.15    [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),
     3.1 --- a/src/FOLP/simp.ML	Sun Feb 07 19:31:55 2010 +0100
     3.2 +++ b/src/FOLP/simp.ML	Sun Feb 07 19:33:34 2010 +0100
     3.3 @@ -519,7 +519,7 @@
     3.4  (* Compute Congruence rules for individual constants using the substition
     3.5     rules *)
     3.6  
     3.7 -val subst_thms = map Drule.standard subst_thms;
     3.8 +val subst_thms = map Drule.export_without_context subst_thms;
     3.9  
    3.10  
    3.11  fun exp_app(0,t) = t
     4.1 --- a/src/HOL/Import/hol4rews.ML	Sun Feb 07 19:31:55 2010 +0100
     4.2 +++ b/src/HOL/Import/hol4rews.ML	Sun Feb 07 19:33:34 2010 +0100
     4.3 @@ -371,7 +371,7 @@
     4.4      fun process ((bthy,bthm), hth as (_,thm)) thy =
     4.5        let
     4.6          val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm);
     4.7 -        val thm2 = Drule.standard thm1;
     4.8 +        val thm2 = Drule.export_without_context thm1;
     4.9        in
    4.10          thy
    4.11          |> PureThy.store_thm (Binding.name bthm, thm2)
     5.1 --- a/src/HOL/Import/shuffler.ML	Sun Feb 07 19:31:55 2010 +0100
     5.2 +++ b/src/HOL/Import/shuffler.ML	Sun Feb 07 19:33:34 2010 +0100
     5.3 @@ -100,7 +100,7 @@
     5.4          val th4 = implies_elim_list (assume cPPQ) [th3,th3]
     5.5                                      |> implies_intr_list [cPPQ,cP]
     5.6      in
     5.7 -        equal_intr th4 th1 |> Drule.standard
     5.8 +        equal_intr th4 th1 |> Drule.export_without_context
     5.9      end
    5.10  
    5.11  val imp_comm =
    5.12 @@ -120,7 +120,7 @@
    5.13          val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP]
    5.14                                      |> implies_intr_list [cQPR,cP,cQ]
    5.15      in
    5.16 -        equal_intr th1 th2 |> Drule.standard
    5.17 +        equal_intr th1 th2 |> Drule.export_without_context
    5.18      end
    5.19  
    5.20  val def_norm =
    5.21 @@ -147,7 +147,7 @@
    5.22                                |> forall_intr cv
    5.23                                |> implies_intr cPQ
    5.24      in
    5.25 -        equal_intr th1 th2 |> Drule.standard
    5.26 +        equal_intr th1 th2 |> Drule.export_without_context
    5.27      end
    5.28  
    5.29  val all_comm =
    5.30 @@ -173,7 +173,7 @@
    5.31                           |> forall_intr_list [cy,cx]
    5.32                           |> implies_intr cl
    5.33      in
    5.34 -        equal_intr th1 th2 |> Drule.standard
    5.35 +        equal_intr th1 th2 |> Drule.export_without_context
    5.36      end
    5.37  
    5.38  val equiv_comm =
    5.39 @@ -187,7 +187,7 @@
    5.40          val th1  = assume ctu |> symmetric |> implies_intr ctu
    5.41          val th2  = assume cut |> symmetric |> implies_intr cut
    5.42      in
    5.43 -        equal_intr th1 th2 |> Drule.standard
    5.44 +        equal_intr th1 th2 |> Drule.export_without_context
    5.45      end
    5.46  
    5.47  (* This simplification procedure rewrites !!x y. P x y
     6.1 --- a/src/HOL/Matrix/cplex/matrixlp.ML	Sun Feb 07 19:31:55 2010 +0100
     6.2 +++ b/src/HOL/Matrix/cplex/matrixlp.ML	Sun Feb 07 19:33:34 2010 +0100
     6.3 @@ -18,7 +18,7 @@
     6.4  
     6.5  fun inst_real thm =
     6.6    let val certT = ctyp_of (Thm.theory_of_thm thm) in
     6.7 -    Drule.standard (Thm.instantiate
     6.8 +    Drule.export_without_context (Thm.instantiate
     6.9        ([(certT (TVar (hd (OldTerm.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
    6.10    end
    6.11  
    6.12 @@ -59,7 +59,7 @@
    6.13          val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
    6.14          val v = TVar (hd (sort ord (OldTerm.term_tvars (prop_of thm))))
    6.15      in
    6.16 -        Drule.standard (Thm.instantiate ([(certT v, certT ty)], []) thm)
    6.17 +        Drule.export_without_context (Thm.instantiate ([(certT v, certT ty)], []) thm)
    6.18      end
    6.19  
    6.20  fun inst_tvars [] thms = thms
     7.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sun Feb 07 19:31:55 2010 +0100
     7.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Feb 07 19:33:34 2010 +0100
     7.3 @@ -152,7 +152,7 @@
     7.4  
     7.5  fun projections rule =
     7.6    Project_Rule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
     7.7 -  |> map (Drule.standard #> Rule_Cases.save rule);
     7.8 +  |> map (Drule.export_without_context #> Rule_Cases.save rule);
     7.9  
    7.10  val supp_prod = thm "supp_prod";
    7.11  val fresh_prod = thm "fresh_prod";
    7.12 @@ -312,7 +312,7 @@
    7.13  
    7.14      val unfolded_perm_eq_thms =
    7.15        if length descr = length new_type_names then []
    7.16 -      else map Drule.standard (List.drop (split_conj_thm
    7.17 +      else map Drule.export_without_context (List.drop (split_conj_thm
    7.18          (Goal.prove_global thy2 [] []
    7.19            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    7.20              (map (fn (c as (s, T), x) =>
    7.21 @@ -332,7 +332,7 @@
    7.22  
    7.23      val perm_empty_thms = maps (fn a =>
    7.24        let val permT = mk_permT (Type (a, []))
    7.25 -      in map Drule.standard (List.take (split_conj_thm
    7.26 +      in map Drule.export_without_context (List.take (split_conj_thm
    7.27          (Goal.prove_global thy2 [] []
    7.28            (augment_sort thy2 [pt_class_of thy2 a]
    7.29              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    7.30 @@ -364,7 +364,7 @@
    7.31          val pt_inst = pt_inst_of thy2 a;
    7.32          val pt2' = pt_inst RS pt2;
    7.33          val pt2_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
    7.34 -      in List.take (map Drule.standard (split_conj_thm
    7.35 +      in List.take (map Drule.export_without_context (split_conj_thm
    7.36          (Goal.prove_global thy2 [] []
    7.37             (augment_sort thy2 [pt_class_of thy2 a]
    7.38               (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    7.39 @@ -399,7 +399,7 @@
    7.40          val pt3' = pt_inst RS pt3;
    7.41          val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
    7.42          val pt3_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
    7.43 -      in List.take (map Drule.standard (split_conj_thm
    7.44 +      in List.take (map Drule.export_without_context (split_conj_thm
    7.45          (Goal.prove_global thy2 [] []
    7.46            (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
    7.47               (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
    7.48 @@ -586,7 +586,7 @@
    7.49        (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
    7.50        (perm_indnames ~~ descr);
    7.51  
    7.52 -    fun mk_perm_closed name = map (fn th => Drule.standard (th RS mp))
    7.53 +    fun mk_perm_closed name = map (fn th => Drule.export_without_context (th RS mp))
    7.54        (List.take (split_conj_thm (Goal.prove_global thy4 [] []
    7.55          (augment_sort thy4
    7.56            (pt_class_of thy4 name :: map (cp_class_of thy4 name) (remove (op =) name dt_atoms))
    7.57 @@ -812,7 +812,8 @@
    7.58          val rep_const = cterm_of thy
    7.59            (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
    7.60          val dist =
    7.61 -          Drule.standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    7.62 +          Drule.export_without_context
    7.63 +            (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    7.64          val (thy', defs', eqns') = fold (make_constr_def tname T T')
    7.65            (constrs ~~ constrs' ~~ constr_syntax) (Sign.add_path tname thy, defs, [])
    7.66        in
    7.67 @@ -877,8 +878,9 @@
    7.68            let
    7.69              val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
    7.70                simp_tac (global_simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
    7.71 -          in dist_thm :: Drule.standard (dist_thm RS not_sym) ::
    7.72 -            prove_distinct_thms p (k, ts)
    7.73 +          in
    7.74 +            dist_thm :: Drule.export_without_context (dist_thm RS not_sym) ::
    7.75 +              prove_distinct_thms p (k, ts)
    7.76            end;
    7.77  
    7.78      val distinct_thms = map2 prove_distinct_thms
    7.79 @@ -1092,7 +1094,7 @@
    7.80  
    7.81      val finite_supp_thms = map (fn atom =>
    7.82        let val atomT = Type (atom, [])
    7.83 -      in map Drule.standard (List.take
    7.84 +      in map Drule.export_without_context (List.take
    7.85          (split_conj_thm (Goal.prove_global thy8 [] []
    7.86             (augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort)
    7.87               (HOLogic.mk_Trueprop
    7.88 @@ -1540,7 +1542,7 @@
    7.89            in
    7.90              (R $ x $ y, R' $ mk_perm [] pi x $ mk_perm [] pi y)
    7.91            end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs));
    7.92 -        val ths = map (fn th => Drule.standard (th RS mp)) (split_conj_thm
    7.93 +        val ths = map (fn th => Drule.export_without_context (th RS mp)) (split_conj_thm
    7.94            (Goal.prove_global thy11 [] []
    7.95              (augment_sort thy1 pt_cp_sort
    7.96                (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
    7.97 @@ -1572,7 +1574,7 @@
    7.98            (finite $ (Const ("Nominal.supp", T --> aset) $ f)))
    7.99              (rec_fns ~~ rec_fn_Ts)
   7.100        in
   7.101 -        map (fn th => Drule.standard (th RS mp)) (split_conj_thm
   7.102 +        map (fn th => Drule.export_without_context (th RS mp)) (split_conj_thm
   7.103            (Goal.prove_global thy11 []
   7.104              (map (augment_sort thy11 fs_cp_sort) fins)
   7.105              (augment_sort thy11 fs_cp_sort
   7.106 @@ -1615,7 +1617,7 @@
   7.107              val y = Free ("y", U);
   7.108              val y' = Free ("y'", U)
   7.109            in
   7.110 -            Drule.standard (Goal.prove (ProofContext.init thy11) []
   7.111 +            Drule.export_without_context (Goal.prove (ProofContext.init thy11) []
   7.112                (map (augment_sort thy11 fs_cp_sort)
   7.113                  (finite_prems @
   7.114                     [HOLogic.mk_Trueprop (R $ x $ y),
   7.115 @@ -2060,7 +2062,7 @@
   7.116           ((Binding.name "rec_equiv'", flat rec_equiv_thms'), []),
   7.117           ((Binding.name "rec_fin_supp", flat rec_fin_supp_thms), []),
   7.118           ((Binding.name "rec_fresh", flat rec_fresh_thms), []),
   7.119 -         ((Binding.name "rec_unique", map Drule.standard rec_unique_thms), []),
   7.120 +         ((Binding.name "rec_unique", map Drule.export_without_context rec_unique_thms), []),
   7.121           ((Binding.name "recs", rec_thms), [])] ||>
   7.122        Sign.parent_path ||>
   7.123        map_nominal_datatypes (fold Symtab.update dt_infos);
     8.1 --- a/src/HOL/Statespace/state_fun.ML	Sun Feb 07 19:31:55 2010 +0100
     8.2 +++ b/src/HOL/Statespace/state_fun.ML	Sun Feb 07 19:33:34 2010 +0100
     8.3 @@ -310,7 +310,7 @@
     8.4                    val prop = list_all ([("n",nT),("x",eT)],
     8.5                                Logic.mk_equals (Const ("Ex",Tex)$Abs(s,T,eq),
     8.6                                                 HOLogic.true_const));
     8.7 -                  val thm = Drule.standard (prove prop);
     8.8 +                  val thm = Drule.export_without_context (prove prop);
     8.9                    val thm' = if swap then swap_ex_eq OF [thm] else thm
    8.10               in SOME thm' end
    8.11               handle TERM _ => NONE)
     9.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sun Feb 07 19:31:55 2010 +0100
     9.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Feb 07 19:33:34 2010 +0100
     9.3 @@ -253,9 +253,11 @@
     9.4          val rep_const = cterm_of thy
     9.5            (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> Univ_elT));
     9.6          val cong' =
     9.7 -          Drule.standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
     9.8 +          Drule.export_without_context
     9.9 +            (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
    9.10          val dist =
    9.11 -          Drule.standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    9.12 +          Drule.export_without_context
    9.13 +            (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    9.14          val (thy', defs', eqns', _) = fold ((make_constr_def tname T) (length constrs))
    9.15            (constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1);
    9.16        in
    9.17 @@ -532,7 +534,7 @@
    9.18                let
    9.19                  val dist_thm = Skip_Proof.prove_global thy5 [] [] t (fn _ =>
    9.20                    EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
    9.21 -              in dist_thm :: Drule.standard (dist_thm RS not_sym) :: prove ts end;
    9.22 +              in dist_thm :: Drule.export_without_context (dist_thm RS not_sym) :: prove ts end;
    9.23        in prove ts end;
    9.24  
    9.25      val distinct_thms = map2 (prove_distinct_thms)
    10.1 --- a/src/HOL/Tools/Function/size.ML	Sun Feb 07 19:31:55 2010 +0100
    10.2 +++ b/src/HOL/Tools/Function/size.ML	Sun Feb 07 19:33:34 2010 +0100
    10.3 @@ -197,7 +197,7 @@
    10.4  
    10.5      fun prove_size_eqs p size_fns size_ofp simpset =
    10.6        maps (fn (((_, (_, _, constrs)), size_const), T) =>
    10.7 -        map (fn constr => Drule.standard (Skip_Proof.prove ctxt [] []
    10.8 +        map (fn constr => Drule.export_without_context (Skip_Proof.prove ctxt [] []
    10.9            (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
   10.10               size_ofp size_const T constr)
   10.11            (fn _ => simp_tac simpset 1))) constrs)
    11.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Feb 07 19:31:55 2010 +0100
    11.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Feb 07 19:33:34 2010 +0100
    11.3 @@ -577,7 +577,7 @@
    11.4          (*val elim = singleton (Inductive_Set.codegen_preproc thy) (preprocess_elim thy nparams 
    11.5            (expand_tuples_elim pre_elim))*)
    11.6          val elim =
    11.7 -          (Drule.standard o Skip_Proof.make_thm thy)
    11.8 +          (Drule.export_without_context o Skip_Proof.make_thm thy)
    11.9            (mk_casesrule (ProofContext.init thy) pred intros)
   11.10        in
   11.11          mk_pred_data ((intros, SOME elim), no_compilation)
   11.12 @@ -641,7 +641,7 @@
   11.13        else ()
   11.14      val pred = Const (constname, T)
   11.15      val pre_elim = 
   11.16 -      (Drule.standard o Skip_Proof.make_thm thy)
   11.17 +      (Drule.export_without_context o Skip_Proof.make_thm thy)
   11.18        (mk_casesrule (ProofContext.init thy) pred pre_intros)
   11.19    in register_predicate (constname, pre_intros, pre_elim) thy end
   11.20  
   11.21 @@ -2178,7 +2178,8 @@
   11.22      (join_preds_modes moded_clauses compiled_terms)
   11.23  
   11.24  fun prove_by_skip options thy _ _ _ _ compiled_terms =
   11.25 -  map_preds_modes (fn pred => fn mode => fn t => Drule.standard (Skip_Proof.make_thm thy t))
   11.26 +  map_preds_modes
   11.27 +    (fn pred => fn mode => fn t => Drule.export_without_context (Skip_Proof.make_thm thy t))
   11.28      compiled_terms
   11.29  
   11.30  (* preparation of introduction rules into special datastructures *)
   11.31 @@ -2269,7 +2270,7 @@
   11.32          val elim = the_elim_of thy predname
   11.33          val nparams = nparams_of thy predname
   11.34          val elim' =
   11.35 -          (Drule.standard o (Skip_Proof.make_thm thy))
   11.36 +          (Drule.export_without_context o Skip_Proof.make_thm thy)
   11.37            (mk_casesrule (ProofContext.init thy) nparams intros)
   11.38        in
   11.39          if not (Thm.equiv_thm (elim, elim')) then
    12.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun Feb 07 19:31:55 2010 +0100
    12.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun Feb 07 19:33:34 2010 +0100
    12.3 @@ -391,7 +391,7 @@
    12.4          |> map (fn (concl'::conclprems, _) =>
    12.5            Logic.list_implies ((flat prems') @ conclprems, concl')))
    12.6    in
    12.7 -    map (Drule.standard o (Skip_Proof.make_thm thy)) intro_ts'
    12.8 +    map (Drule.export_without_context o Skip_Proof.make_thm thy) intro_ts'
    12.9    end
   12.10  
   12.11  end;
    13.1 --- a/src/HOL/Tools/TFL/post.ML	Sun Feb 07 19:31:55 2010 +0100
    13.2 +++ b/src/HOL/Tools/TFL/post.ML	Sun Feb 07 19:33:34 2010 +0100
    13.3 @@ -129,7 +129,7 @@
    13.4  
    13.5  (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
    13.6  val meta_outer =
    13.7 -  curry_rule o Drule.standard o
    13.8 +  curry_rule o Drule.export_without_context o
    13.9    rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
   13.10  
   13.11  (*Strip off the outer !P*)
   13.12 @@ -151,7 +151,7 @@
   13.13                 {f = f, R = R, rules = rules,
   13.14                  full_pats_TCs = full_pats_TCs,
   13.15                  TCs = TCs}
   13.16 -       val rules' = map (Drule.standard o ObjectLogic.rulify_no_asm)
   13.17 +       val rules' = map (Drule.export_without_context o ObjectLogic.rulify_no_asm)
   13.18                          (R.CONJUNCTS rules)
   13.19           in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
   13.20          rules = ListPair.zip(rules', rows),
   13.21 @@ -180,7 +180,7 @@
   13.22      | solve_eq (th, [a], i) = [(a, i)]
   13.23      | solve_eq (th, splitths as (_ :: _), i) = 
   13.24        (writeln "Proving unsplit equation...";
   13.25 -      [((Drule.standard o ObjectLogic.rulify_no_asm)
   13.26 +      [((Drule.export_without_context o ObjectLogic.rulify_no_asm)
   13.27            (CaseSplit.splitto splitths th), i)])
   13.28        (* if there's an error, pretend nothing happened with this definition 
   13.29           We should probably print something out so that the user knows...? *)
   13.30 @@ -236,7 +236,7 @@
   13.31   in (theory,
   13.32       (*return the conjoined induction rule and recursion equations,
   13.33         with assumptions remaining to discharge*)
   13.34 -     Drule.standard (induction RS (rules RS conjI)))
   13.35 +     Drule.export_without_context (induction RS (rules RS conjI)))
   13.36   end
   13.37  
   13.38  fun defer thy congs fid seqs =
    14.1 --- a/src/HOL/Tools/arith_data.ML	Sun Feb 07 19:31:55 2010 +0100
    14.2 +++ b/src/HOL/Tools/arith_data.ML	Sun Feb 07 19:33:34 2010 +0100
    14.3 @@ -110,8 +110,8 @@
    14.4  
    14.5  fun prove_conv tacs ctxt (_: thm list) = prove_conv_nohyps tacs ctxt;
    14.6  
    14.7 -fun prove_conv2 expand_tac norm_tac ss tu = (*FIXME avoid standard*)
    14.8 -  mk_meta_eq (Drule.standard (Goal.prove (Simplifier.the_context ss) [] []
    14.9 +fun prove_conv2 expand_tac norm_tac ss tu = (* FIXME avoid Drule.export_without_context *)
   14.10 +  mk_meta_eq (Drule.export_without_context (Goal.prove (Simplifier.the_context ss) [] []
   14.11        (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
   14.12      (K (EVERY [expand_tac, norm_tac ss]))));
   14.13  
    15.1 --- a/src/HOL/Tools/choice_specification.ML	Sun Feb 07 19:31:55 2010 +0100
    15.2 +++ b/src/HOL/Tools/choice_specification.ML	Sun Feb 07 19:33:34 2010 +0100
    15.3 @@ -75,7 +75,7 @@
    15.4  fun add_specification axiomatic cos arg =
    15.5      arg |> apsnd Thm.freezeT
    15.6          |> proc_exprop axiomatic cos
    15.7 -        |> apsnd Drule.standard
    15.8 +        |> apsnd Drule.export_without_context
    15.9  
   15.10  
   15.11  (* Collect all intances of constants in term *)
   15.12 @@ -189,7 +189,7 @@
   15.13                      in
   15.14                          args |> apsnd (remove_alls frees)
   15.15                               |> apsnd undo_imps
   15.16 -                             |> apsnd Drule.standard
   15.17 +                             |> apsnd Drule.export_without_context
   15.18                               |> Thm.theory_attributes (map (Attrib.attribute thy) atts)
   15.19                               |> add_final
   15.20                               |> Library.swap
    16.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sun Feb 07 19:31:55 2010 +0100
    16.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sun Feb 07 19:33:34 2010 +0100
    16.3 @@ -544,7 +544,7 @@
    16.4        (fn NONE => "X" | SOME k' => string_of_int k')
    16.5          (ks @ [SOME k]))) arities));
    16.6  
    16.7 -fun prep_intrs intrs = map (rename_term o #prop o rep_thm o Drule.standard) intrs;
    16.8 +fun prep_intrs intrs = map (rename_term o #prop o rep_thm o Drule.export_without_context) intrs;
    16.9  
   16.10  fun constrain cs [] = []
   16.11    | constrain cs ((s, xs) :: ys) =
    17.1 --- a/src/HOL/Tools/record.ML	Sun Feb 07 19:31:55 2010 +0100
    17.2 +++ b/src/HOL/Tools/record.ML	Sun Feb 07 19:33:34 2010 +0100
    17.3 @@ -1014,7 +1014,7 @@
    17.4      else if Goal.future_enabled () then
    17.5        Goal.future_result (ProofContext.init thy) (Future.fork_pri ~1 prf) prop
    17.6      else prf ()
    17.7 -  in Drule.standard thm end;
    17.8 +  in Drule.export_without_context thm end;
    17.9  
   17.10  fun prove_common immediate stndrd thy asms prop tac =
   17.11    let
   17.12 @@ -1023,7 +1023,7 @@
   17.13        else if immediate orelse not (Goal.future_enabled ()) then Goal.prove
   17.14        else Goal.prove_future;
   17.15      val prf = prv (ProofContext.init thy) [] asms prop tac;
   17.16 -  in if stndrd then Drule.standard prf else prf end;
   17.17 +  in if stndrd then Drule.export_without_context prf else prf end;
   17.18  
   17.19  val prove_future_global = prove_common false;
   17.20  val prove_global = prove_common true;
   17.21 @@ -1072,7 +1072,7 @@
   17.22            if is_sel_upd_pair thy acc upd
   17.23            then o_eq_dest
   17.24            else o_eq_id_dest;
   17.25 -      in Drule.standard (othm RS dest) end;
   17.26 +      in Drule.export_without_context (othm RS dest) end;
   17.27    in map get_simp upd_funs end;
   17.28  
   17.29  fun get_updupd_simp thy defset u u' comp =
   17.30 @@ -1092,7 +1092,7 @@
   17.31            REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
   17.32            TRY (simp_tac (HOL_ss addsimps [id_apply]) 1));
   17.33      val dest = if comp then o_eq_dest_lhs else o_eq_dest;
   17.34 -  in Drule.standard (othm RS dest) end;
   17.35 +  in Drule.export_without_context (othm RS dest) end;
   17.36  
   17.37  fun get_updupd_simps thy term defset =
   17.38    let
   17.39 @@ -1279,8 +1279,8 @@
   17.40              val ss = get_sel_upd_defs thy;
   17.41              val uathm = get_upd_acc_cong_thm upd acc thy ss;
   17.42            in
   17.43 -           [Drule.standard (uathm RS updacc_noopE),
   17.44 -            Drule.standard (uathm RS updacc_noop_compE)]
   17.45 +           [Drule.export_without_context (uathm RS updacc_noopE),
   17.46 +            Drule.export_without_context (uathm RS updacc_noop_compE)]
   17.47            end;
   17.48  
   17.49          (*If f is constant then (f o g) = f.  We know that K_skeleton
   17.50 @@ -1721,8 +1721,8 @@
   17.51        to prove other theorems. We haven't given names to the accessors
   17.52        f, g etc yet however, so we generate an ext structure with
   17.53        free variables as all arguments and allow the introduction tactic to
   17.54 -      operate on it as far as it can. We then use Drule.standard to convert
   17.55 -      the free variables into unifiable variables and unify them with
   17.56 +      operate on it as far as it can. We then use Drule.export_without_context
   17.57 +      to convert the free variables into unifiable variables and unify them with
   17.58        (roughly) the definition of the accessor.*)
   17.59      fun surject_prf () =
   17.60        let
   17.61 @@ -1733,7 +1733,7 @@
   17.62            REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1;
   17.63          val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
   17.64          val [halfway] = Seq.list_of (tactic1 start);
   17.65 -        val [surject] = Seq.list_of (tactic2 (Drule.standard halfway));
   17.66 +        val [surject] = Seq.list_of (tactic2 (Drule.export_without_context halfway));
   17.67        in
   17.68          surject
   17.69        end;
   17.70 @@ -2136,14 +2136,14 @@
   17.71      fun sel_convs_prf () =
   17.72        map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props;
   17.73      val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
   17.74 -    fun sel_convs_standard_prf () = map Drule.standard sel_convs
   17.75 +    fun sel_convs_standard_prf () = map Drule.export_without_context sel_convs;
   17.76      val sel_convs_standard =
   17.77        timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
   17.78  
   17.79      fun upd_convs_prf () =
   17.80        map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props;
   17.81      val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
   17.82 -    fun upd_convs_standard_prf () = map Drule.standard upd_convs
   17.83 +    fun upd_convs_standard_prf () = map Drule.export_without_context upd_convs;
   17.84      val upd_convs_standard =
   17.85        timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
   17.86  
   17.87 @@ -2151,7 +2151,7 @@
   17.88        let
   17.89          val symdefs = map symmetric (sel_defs @ upd_defs);
   17.90          val fold_ss = HOL_basic_ss addsimps symdefs;
   17.91 -        val ua_congs = map (Drule.standard o simplify fold_ss) upd_acc_cong_assists;
   17.92 +        val ua_congs = map (Drule.export_without_context o simplify fold_ss) upd_acc_cong_assists;
   17.93        in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
   17.94      val (fold_congs, unfold_congs) =
   17.95        timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
   17.96 @@ -2221,7 +2221,7 @@
   17.97              rtac (prop_subst OF [surjective]),
   17.98              REPEAT o etac meta_allE, atac]);
   17.99      val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
  17.100 -    fun split_meta_standardise () = Drule.standard split_meta;
  17.101 +    fun split_meta_standardise () = Drule.export_without_context split_meta;
  17.102      val split_meta_standard =
  17.103        timeit_msg "record split_meta standard:" split_meta_standardise;
  17.104  
    18.1 --- a/src/HOL/Tools/split_rule.ML	Sun Feb 07 19:31:55 2010 +0100
    18.2 +++ b/src/HOL/Tools/split_rule.ML	Sun Feb 07 19:33:34 2010 +0100
    18.3 @@ -100,13 +100,13 @@
    18.4        | (t, ts) => fold collect_vars ts);
    18.5  
    18.6  
    18.7 -val split_rule_var = (Drule.standard o remove_internal_split) oo split_rule_var';
    18.8 +val split_rule_var = (Drule.export_without_context o remove_internal_split) oo split_rule_var';
    18.9  
   18.10  (*curries ALL function variables occurring in a rule's conclusion*)
   18.11  fun split_rule rl =
   18.12    fold_rev split_rule_var' (OldTerm.term_vars (concl_of rl)) rl
   18.13    |> remove_internal_split
   18.14 -  |> Drule.standard;
   18.15 +  |> Drule.export_without_context;
   18.16  
   18.17  (*curries ALL function variables*)
   18.18  fun complete_split_rule rl =
   18.19 @@ -117,7 +117,7 @@
   18.20    in
   18.21      fst (fold_rev complete_split_rule_var vars (rl, xs))
   18.22      |> remove_internal_split
   18.23 -    |> Drule.standard
   18.24 +    |> Drule.export_without_context
   18.25      |> Rule_Cases.save rl
   18.26    end;
   18.27  
   18.28 @@ -137,7 +137,7 @@
   18.29      rl
   18.30      |> fold_index one_goal xss
   18.31      |> Simplifier.full_simplify split_rule_ss
   18.32 -    |> Drule.standard
   18.33 +    |> Drule.export_without_context
   18.34      |> Rule_Cases.save rl
   18.35    end;
   18.36  
    19.1 --- a/src/HOL/Tools/typedef.ML	Sun Feb 07 19:31:55 2010 +0100
    19.2 +++ b/src/HOL/Tools/typedef.ML	Sun Feb 07 19:33:34 2010 +0100
    19.3 @@ -122,7 +122,7 @@
    19.4            let
    19.5              val cert = Thm.cterm_of (Thm.theory_of_thm def_eq);
    19.6              val goal_eq = MetaSimplifier.rewrite true [def_eq] (cert goal');
    19.7 -          in Drule.standard (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
    19.8 +          in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
    19.9  
   19.10      fun typedef_result inhabited =
   19.11        ObjectLogic.typedecl (t, vs, mx)
   19.12 @@ -139,7 +139,7 @@
   19.13        ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps
   19.14        #-> (fn ([type_definition], set_def) => fn thy1 =>
   19.15          let
   19.16 -          fun make th = Drule.standard (th OF [type_definition]);
   19.17 +          fun make th = Drule.export_without_context (th OF [type_definition]);
   19.18            val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
   19.19                Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) =
   19.20              thy1
    20.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Feb 07 19:31:55 2010 +0100
    20.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Feb 07 19:33:34 2010 +0100
    20.3 @@ -251,7 +251,7 @@
    20.4  
    20.5      (* register unfold theorems *)
    20.6      val (unfold_thms, thy) =
    20.7 -      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard))
    20.8 +      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context))
    20.9          (mk_unfold_thms unfold_binds tuple_unfold_thm) thy;
   20.10    in
   20.11      ((proj_thms, unfold_thms), thy)
   20.12 @@ -446,7 +446,7 @@
   20.13      (* prove isomorphism and isodefl rules *)
   20.14      fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy =
   20.15        let
   20.16 -        fun make thm = Drule.standard (thm OF [REP_eq, abs_def, rep_def]);
   20.17 +        fun make thm = Drule.export_without_context (thm OF [REP_eq, abs_def, rep_def]);
   20.18          val rep_iso_thm = make @{thm domain_rep_iso};
   20.19          val abs_iso_thm = make @{thm domain_abs_iso};
   20.20          val isodefl_thm = make @{thm isodefl_abs_rep};
   20.21 @@ -545,7 +545,7 @@
   20.22            val thmR = thm RS @{thm conjunct2};
   20.23          in (n, thmL):: conjuncts ns thmR end;
   20.24      val (isodefl_thms, thy) = thy |>
   20.25 -      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard))
   20.26 +      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context))
   20.27          (conjuncts isodefl_binds isodefl_thm);
   20.28      val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy;
   20.29  
    21.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Feb 07 19:31:55 2010 +0100
    21.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Feb 07 19:33:34 2010 +0100
    21.3 @@ -180,7 +180,7 @@
    21.4  val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
    21.5  val abs_defin' = iso_locale RS iso_abs_defin';
    21.6  val rep_defin' = iso_locale RS iso_rep_defin';
    21.7 -val iso_rews = map Drule.standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
    21.8 +val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
    21.9  
   21.10  (* ----- generating beta reduction rules from definitions-------------------- *)
   21.11  
   21.12 @@ -263,7 +263,7 @@
   21.13    val exhaust = pg con_appls (mk_trp exh) (K tacs);
   21.14    val _ = trace " Proving casedist...";
   21.15    val casedist =
   21.16 -    Drule.standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
   21.17 +    Drule.export_without_context (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
   21.18  end;
   21.19  
   21.20  local 
   21.21 @@ -554,7 +554,7 @@
   21.22          flat
   21.23            (ListPair.map (distinct c) ((map #1 cs),leqs)) @
   21.24          distincts cs;
   21.25 -  in map Drule.standard (distincts (cons ~~ distincts_le)) end;
   21.26 +  in map Drule.export_without_context (distincts (cons ~~ distincts_le)) end;
   21.27  
   21.28  local 
   21.29    fun pgterm rel con args =
   21.30 @@ -755,7 +755,7 @@
   21.31          maps (eq_tacs ctxt) eqs;
   21.32      in pg copy_take_defs goal tacs end;
   21.33  in
   21.34 -  val take_rews = map Drule.standard
   21.35 +  val take_rews = map Drule.export_without_context
   21.36      (atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps);
   21.37  end; (* local *)
   21.38  
    22.1 --- a/src/HOLCF/Tools/pcpodef.ML	Sun Feb 07 19:31:55 2010 +0100
    22.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Sun Feb 07 19:33:34 2010 +0100
    22.3 @@ -89,7 +89,7 @@
    22.4            (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
    22.5      (* transfer thms so that they will know about the new cpo instance *)
    22.6      val cpo_thms' = map (Thm.transfer thy2) cpo_thms;
    22.7 -    fun make thm = Drule.standard (thm OF cpo_thms');
    22.8 +    fun make thm = Drule.export_without_context (thm OF cpo_thms');
    22.9      val ([adm, cont_Rep, cont_Abs, lub, thelub, compact], thy3) =
   22.10        thy2
   22.11        |> Sign.add_path (Binding.name_of name)
   22.12 @@ -127,7 +127,7 @@
   22.13        |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
   22.14          (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
   22.15      val pcpo_thms' = map (Thm.transfer thy2) pcpo_thms;
   22.16 -    fun make thm = Drule.standard (thm OF pcpo_thms');
   22.17 +    fun make thm = Drule.export_without_context (thm OF pcpo_thms');
   22.18      val ([Rep_strict, Abs_strict, Rep_strict_iff, Abs_strict_iff,
   22.19            Rep_defined, Abs_defined], thy3) =
   22.20        thy2
    23.1 --- a/src/HOLCF/Tools/repdef.ML	Sun Feb 07 19:31:55 2010 +0100
    23.2 +++ b/src/HOLCF/Tools/repdef.ML	Sun Feb 07 19:33:34 2010 +0100
    23.3 @@ -139,7 +139,7 @@
    23.4        |> Sign.add_path (Binding.name_of name)
    23.5        |> PureThy.add_thms
    23.6          [((Binding.prefix_name "REP_" name,
    23.7 -          Drule.standard (@{thm typedef_REP} OF typedef_thms')), [])]
    23.8 +          Drule.export_without_context (@{thm typedef_REP} OF typedef_thms')), [])]
    23.9        ||> Sign.parent_path;
   23.10  
   23.11      val rep_info =
    24.1 --- a/src/Provers/hypsubst.ML	Sun Feb 07 19:31:55 2010 +0100
    24.2 +++ b/src/Provers/hypsubst.ML	Sun Feb 07 19:33:34 2010 +0100
    24.3 @@ -165,7 +165,7 @@
    24.4  
    24.5  end;
    24.6  
    24.7 -val ssubst = Drule.standard (Data.sym RS Data.subst);
    24.8 +val ssubst = Drule.export_without_context (Data.sym RS Data.subst);
    24.9  
   24.10  fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
   24.11    case try (Logic.strip_assums_hyp #> hd #>
    25.1 --- a/src/Provers/typedsimp.ML	Sun Feb 07 19:31:55 2010 +0100
    25.2 +++ b/src/Provers/typedsimp.ML	Sun Feb 07 19:33:34 2010 +0100
    25.3 @@ -43,11 +43,11 @@
    25.4  (*For simplifying both sides of an equation:
    25.5        [| a=c; b=c |] ==> b=a
    25.6    Can use resolve_tac [split_eqn] to prepare an equation for simplification. *)
    25.7 -val split_eqn = Drule.standard (sym RSN (2,trans) RS sym);
    25.8 +val split_eqn = Drule.export_without_context (sym RSN (2,trans) RS sym);
    25.9  
   25.10  
   25.11  (*    [| a=b; b=c |] ==> reduce(a,c)  *)
   25.12 -val red_trans = Drule.standard (trans RS red_if_equal);
   25.13 +val red_trans = Drule.export_without_context (trans RS red_if_equal);
   25.14  
   25.15  (*For REWRITE rule: Make a reduction rule for simplification, e.g.
   25.16    [| a: C(0); ... ; a=c: C(0) |] ==> rec(0,a,b) = c: C(0) *)
    26.1 --- a/src/Pure/Isar/attrib.ML	Sun Feb 07 19:31:55 2010 +0100
    26.2 +++ b/src/Pure/Isar/attrib.ML	Sun Feb 07 19:33:34 2010 +0100
    26.3 @@ -298,7 +298,7 @@
    26.4    setup (Binding.name "params")
    26.5      (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
    26.6      "named rule parameters" #>
    26.7 -  setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.standard)))
    26.8 +  setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.export_without_context)))
    26.9      "result put into standard form (legacy)" #>
   26.10    setup (Binding.name "rule_format") rule_format "result put into canonical rule format" #>
   26.11    setup (Binding.name "elim_format") (Scan.succeed elim_format)
    27.1 --- a/src/Pure/Isar/class.ML	Sun Feb 07 19:31:55 2010 +0100
    27.2 +++ b/src/Pure/Isar/class.ML	Sun Feb 07 19:33:34 2010 +0100
    27.3 @@ -86,7 +86,7 @@
    27.4        | SOME prop => Logic.mk_implies (Morphism.term const_morph
    27.5            ((map_types o map_atyps) (K aT) prop), of_class_prop_concl);
    27.6      val sup_of_classes = map (snd o rules thy) sups;
    27.7 -    val loc_axiom_intros = map Drule.standard' (Locale.axioms_of thy class);
    27.8 +    val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
    27.9      val axclass_intro = #intro (AxClass.get_info thy class);
   27.10      val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
   27.11      val tac = REPEAT (SOMEGOAL
    28.1 --- a/src/Pure/Isar/class_target.ML	Sun Feb 07 19:31:55 2010 +0100
    28.2 +++ b/src/Pure/Isar/class_target.ML	Sun Feb 07 19:33:34 2010 +0100
    28.3 @@ -233,7 +233,7 @@
    28.4  fun register_subclass (sub, sup) some_dep_morph some_wit export thy =
    28.5    let
    28.6      val intros = (snd o rules thy) sup :: map_filter I
    28.7 -      [Option.map (Drule.standard' o Element.conclude_witness) some_wit,
    28.8 +      [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit,
    28.9          (fst o rules thy) sub];
   28.10      val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
   28.11      val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
    29.1 --- a/src/Pure/Isar/expression.ML	Sun Feb 07 19:31:55 2010 +0100
    29.2 +++ b/src/Pure/Isar/expression.ML	Sun Feb 07 19:33:34 2010 +0100
    29.3 @@ -699,7 +699,7 @@
    29.4              |> PureThy.note_thmss ""
    29.5                   [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
    29.6                    ((Binding.conceal (Binding.name axiomsN), []),
    29.7 -                    [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
    29.8 +                    [(map (Drule.export_without_context o Element.conclude_witness) axioms, [])])]
    29.9              ||> Sign.restore_naming thy''';
   29.10          in (SOME statement, SOME intro, axioms, thy'''') end;
   29.11    in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;
    30.1 --- a/src/Pure/Isar/skip_proof.ML	Sun Feb 07 19:31:55 2010 +0100
    30.2 +++ b/src/Pure/Isar/skip_proof.ML	Sun Feb 07 19:33:34 2010 +0100
    30.3 @@ -39,6 +39,6 @@
    30.4        else tac args st);
    30.5  
    30.6  fun prove_global thy xs asms prop tac =
    30.7 -  Drule.standard (prove (ProofContext.init thy) xs asms prop tac);
    30.8 +  Drule.export_without_context (prove (ProofContext.init thy) xs asms prop tac);
    30.9  
   30.10  end;
    31.1 --- a/src/Pure/ML/ml_context.ML	Sun Feb 07 19:31:55 2010 +0100
    31.2 +++ b/src/Pure/ML/ml_context.ML	Sun Feb 07 19:33:34 2010 +0100
    31.3 @@ -70,8 +70,8 @@
    31.4  val ml_store_thms = ml_store "";
    31.5  fun ml_store_thm (name, th) = ml_store "hd" (name, [th]);
    31.6  
    31.7 -fun bind_thm (name, thm) = ml_store_thm (name, Drule.standard thm);
    31.8 -fun bind_thms (name, thms) = ml_store_thms (name, map Drule.standard thms);
    31.9 +fun bind_thm (name, thm) = ml_store_thm (name, Drule.export_without_context thm);
   31.10 +fun bind_thms (name, thms) = ml_store_thms (name, map Drule.export_without_context thms);
   31.11  
   31.12  fun thm name = ProofContext.get_thm (the_local_context ()) name;
   31.13  fun thms name = ProofContext.get_thms (the_local_context ()) name;
    32.1 --- a/src/Pure/axclass.ML	Sun Feb 07 19:31:55 2010 +0100
    32.2 +++ b/src/Pure/axclass.ML	Sun Feb 07 19:33:34 2010 +0100
    32.3 @@ -484,10 +484,10 @@
    32.4        def_thy
    32.5        |> Sign.mandatory_path (Binding.name_of bconst)
    32.6        |> PureThy.note_thmss ""
    32.7 -        [((Binding.name introN, []), [([Drule.standard raw_intro], [])]),
    32.8 -         ((Binding.name superN, []), [(map Drule.standard raw_classrel, [])]),
    32.9 +        [((Binding.name introN, []), [([Drule.export_without_context raw_intro], [])]),
   32.10 +         ((Binding.name superN, []), [(map Drule.export_without_context raw_classrel, [])]),
   32.11           ((Binding.name axiomsN, []),
   32.12 -           [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
   32.13 +           [(map (fn th => Drule.export_without_context (class_triv RS th)) raw_axioms, [])])]
   32.14        ||> Sign.restore_naming def_thy;
   32.15  
   32.16  
    33.1 --- a/src/Pure/drule.ML	Sun Feb 07 19:31:55 2010 +0100
    33.2 +++ b/src/Pure/drule.ML	Sun Feb 07 19:33:34 2010 +0100
    33.3 @@ -75,8 +75,8 @@
    33.4    val beta_conv: cterm -> cterm -> cterm
    33.5    val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
    33.6    val flexflex_unique: thm -> thm
    33.7 -  val standard: thm -> thm
    33.8 -  val standard': thm -> thm
    33.9 +  val export_without_context: thm -> thm
   33.10 +  val export_without_context_open: thm -> thm
   33.11    val get_def: theory -> xstring -> thm
   33.12    val store_thm: binding -> thm -> thm
   33.13    val store_standard_thm: binding -> thm -> thm
   33.14 @@ -303,9 +303,9 @@
   33.15      |  _   => raise THM("flexflex_unique: multiple unifiers", 0, [th]);
   33.16  
   33.17  
   33.18 -(* legacy standard operations *)
   33.19 +(* old-style export without context *)
   33.20  
   33.21 -val standard' =
   33.22 +val export_without_context_open =
   33.23    implies_intr_hyps
   33.24    #> forall_intr_frees
   33.25    #> `Thm.maxidx_of
   33.26 @@ -315,9 +315,9 @@
   33.27      #> zero_var_indexes
   33.28      #> Thm.varifyT);
   33.29  
   33.30 -val standard =
   33.31 +val export_without_context =
   33.32    flexflex_unique
   33.33 -  #> standard'
   33.34 +  #> export_without_context_open
   33.35    #> Thm.close_derivation;
   33.36  
   33.37  
   33.38 @@ -459,8 +459,8 @@
   33.39  fun store_thm_open name th =
   33.40    Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th)));
   33.41  
   33.42 -fun store_standard_thm name th = store_thm name (standard th);
   33.43 -fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
   33.44 +fun store_standard_thm name th = store_thm name (export_without_context th);
   33.45 +fun store_standard_thm_open name thm = store_thm_open name (export_without_context_open thm);
   33.46  
   33.47  val reflexive_thm =
   33.48    let val cx = certify (Var(("x",0),TVar(("'a",0),[])))
   33.49 @@ -708,12 +708,12 @@
   33.50  val protect = Thm.capply (certify Logic.protectC);
   33.51  
   33.52  val protectI =
   33.53 -  store_thm (Binding.conceal (Binding.name "protectI"))
   33.54 -    (standard (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)));
   33.55 +  store_standard_thm (Binding.conceal (Binding.name "protectI"))
   33.56 +    (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A));
   33.57  
   33.58  val protectD =
   33.59 -  store_thm (Binding.conceal (Binding.name "protectD"))
   33.60 -    (standard (Thm.equal_elim prop_def (Thm.assume (protect A))));
   33.61 +  store_standard_thm (Binding.conceal (Binding.name "protectD"))
   33.62 +    (Thm.equal_elim prop_def (Thm.assume (protect A)));
   33.63  
   33.64  val protect_cong =
   33.65    store_standard_thm_open (Binding.name "protect_cong") (Thm.reflexive (protect A));
   33.66 @@ -730,8 +730,8 @@
   33.67  (* term *)
   33.68  
   33.69  val termI =
   33.70 -  store_thm (Binding.conceal (Binding.name "termI"))
   33.71 -    (standard (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))));
   33.72 +  store_standard_thm (Binding.conceal (Binding.name "termI"))
   33.73 +    (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)));
   33.74  
   33.75  fun mk_term ct =
   33.76    let
   33.77 @@ -759,15 +759,14 @@
   33.78  (* sort_constraint *)
   33.79  
   33.80  val sort_constraintI =
   33.81 -  store_thm (Binding.conceal (Binding.name "sort_constraintI"))
   33.82 -    (standard (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T)));
   33.83 +  store_standard_thm (Binding.conceal (Binding.name "sort_constraintI"))
   33.84 +    (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T));
   33.85  
   33.86  val sort_constraint_eq =
   33.87 -  store_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
   33.88 -    (standard
   33.89 -      (Thm.equal_intr
   33.90 -        (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
   33.91 -        (implies_intr_list [A, C] (Thm.assume A))));
   33.92 +  store_standard_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
   33.93 +    (Thm.equal_intr
   33.94 +      (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
   33.95 +      (implies_intr_list [A, C] (Thm.assume A)));
   33.96  
   33.97  end;
   33.98  
   33.99 @@ -983,5 +982,5 @@
  33.100  
  33.101  end;
  33.102  
  33.103 -structure BasicDrule: BASIC_DRULE = Drule;
  33.104 -open BasicDrule;
  33.105 +structure Basic_Drule: BASIC_DRULE = Drule;
  33.106 +open Basic_Drule;
    34.1 --- a/src/Pure/goal.ML	Sun Feb 07 19:31:55 2010 +0100
    34.2 +++ b/src/Pure/goal.ML	Sun Feb 07 19:33:34 2010 +0100
    34.3 @@ -210,7 +210,7 @@
    34.4  fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
    34.5  
    34.6  fun prove_global thy xs asms prop tac =
    34.7 -  Drule.standard (prove (ProofContext.init thy) xs asms prop tac);
    34.8 +  Drule.export_without_context (prove (ProofContext.init thy) xs asms prop tac);
    34.9  
   34.10  
   34.11  
    35.1 --- a/src/Pure/old_goals.ML	Sun Feb 07 19:31:55 2010 +0100
    35.2 +++ b/src/Pure/old_goals.ML	Sun Feb 07 19:33:34 2010 +0100
    35.3 @@ -305,7 +305,7 @@
    35.4              val th = Goal.conclude ath
    35.5              val thy' = Thm.theory_of_thm th
    35.6              val {hyps, prop, ...} = Thm.rep_thm th
    35.7 -            val final_th = Drule.standard th
    35.8 +            val final_th = Drule.export_without_context th
    35.9          in  if not check then final_th
   35.10              else if not (Theory.eq_thy(thy,thy')) then !result_error_fn state
   35.11                  ("Theory of proof state has changed!" ^
   35.12 @@ -512,7 +512,7 @@
   35.13              0 => thm
   35.14            | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
   35.15    in
   35.16 -    Drule.standard (implies_intr_list As
   35.17 +    Drule.export_without_context (implies_intr_list As
   35.18        (check (Seq.pull (EVERY (f asms) (trivial B)))))
   35.19    end;
   35.20  
    36.1 --- a/src/Sequents/simpdata.ML	Sun Feb 07 19:31:55 2010 +0100
    36.2 +++ b/src/Sequents/simpdata.ML	Sun Feb 07 19:33:34 2010 +0100
    36.3 @@ -49,9 +49,9 @@
    36.4  
    36.5  (*Congruence rules for = or <-> (instead of ==)*)
    36.6  fun mk_meta_cong rl =
    36.7 -  Drule.standard(mk_meta_eq (mk_meta_prems rl))
    36.8 -  handle THM _ =>
    36.9 -  error("Premises and conclusion of congruence rules must use =-equality or <->");
   36.10 +  Drule.export_without_context(mk_meta_eq (mk_meta_prems rl))
   36.11 +    handle THM _ =>
   36.12 +      error("Premises and conclusion of congruence rules must use =-equality or <->");
   36.13  
   36.14  
   36.15  (*** Standard simpsets ***)
    37.1 --- a/src/ZF/Tools/datatype_package.ML	Sun Feb 07 19:31:55 2010 +0100
    37.2 +++ b/src/ZF/Tools/datatype_package.ML	Sun Feb 07 19:33:34 2010 +0100
    37.3 @@ -292,7 +292,7 @@
    37.4           rtac case_trans 1,
    37.5           REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]);
    37.6  
    37.7 -  val free_iffs = map Drule.standard (con_defs RL [@{thm def_swap_iff}]);
    37.8 +  val free_iffs = map Drule.export_without_context (con_defs RL [@{thm def_swap_iff}]);
    37.9  
   37.10    val case_eqns = map prove_case_eqn (flat con_ty_lists ~~ case_args ~~ tl con_defs);
   37.11  
   37.12 @@ -338,7 +338,7 @@
   37.13    val constructors =
   37.14        map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
   37.15  
   37.16 -  val free_SEs = map Drule.standard (Ind_Syntax.mk_free_SEs free_iffs);
   37.17 +  val free_SEs = map Drule.export_without_context (Ind_Syntax.mk_free_SEs free_iffs);
   37.18  
   37.19    val {intrs, elim, induct, mutual_induct, ...} = ind_result
   37.20  
    38.1 --- a/src/ZF/Tools/inductive_package.ML	Sun Feb 07 19:31:55 2010 +0100
    38.2 +++ b/src/ZF/Tools/inductive_package.ML	Sun Feb 07 19:33:34 2010 +0100
    38.3 @@ -193,9 +193,9 @@
    38.4          [rtac (@{thm Collect_subset} RS @{thm bnd_monoI}) 1,
    38.5           REPEAT (ares_tac (@{thms basic_monos} @ monos) 1)]);
    38.6  
    38.7 -  val dom_subset = Drule.standard (big_rec_def RS Fp.subs);
    38.8 +  val dom_subset = Drule.export_without_context (big_rec_def RS Fp.subs);
    38.9  
   38.10 -  val unfold = Drule.standard ([big_rec_def, bnd_mono] MRS Fp.Tarski);
   38.11 +  val unfold = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.Tarski);
   38.12  
   38.13    (********)
   38.14    val dummy = writeln "  Proving the introduction rules...";
   38.15 @@ -205,7 +205,7 @@
   38.16    val Part_trans =
   38.17        case rec_names of
   38.18             [_] => asm_rl
   38.19 -         | _   => Drule.standard (@{thm Part_subset} RS @{thm subset_trans});
   38.20 +         | _   => Drule.export_without_context (@{thm Part_subset} RS @{thm subset_trans});
   38.21  
   38.22    (*To type-check recursive occurrences of the inductive sets, possibly
   38.23      enclosed in some monotonic operator M.*)
   38.24 @@ -272,7 +272,7 @@
   38.25      rule_by_tactic
   38.26        (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac ss) THEN basic_elim_tac)
   38.27        (Thm.assume A RS elim)
   38.28 -      |> Drule.standard';
   38.29 +      |> Drule.export_without_context_open;
   38.30  
   38.31    fun induction_rules raw_induct thy =
   38.32     let
   38.33 @@ -503,7 +503,7 @@
   38.34       val Const (@{const_name Trueprop}, _) $ (pred_var $ _) = concl_of induct0
   38.35  
   38.36       val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0)
   38.37 -                  |> Drule.standard
   38.38 +                  |> Drule.export_without_context
   38.39       and mutual_induct = CP.remove_split mutual_induct_fsplit
   38.40  
   38.41       val ([induct', mutual_induct'], thy') =
   38.42 @@ -514,7 +514,7 @@
   38.43      in ((thy', induct'), mutual_induct')
   38.44      end;  (*of induction_rules*)
   38.45  
   38.46 -  val raw_induct = Drule.standard ([big_rec_def, bnd_mono] MRS Fp.induct)
   38.47 +  val raw_induct = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.induct)
   38.48  
   38.49    val ((thy2, induct), mutual_induct) =
   38.50      if not coind then induction_rules raw_induct thy1
    39.1 --- a/src/ZF/ind_syntax.ML	Sun Feb 07 19:31:55 2010 +0100
    39.2 +++ b/src/ZF/ind_syntax.ML	Sun Feb 07 19:33:34 2010 +0100
    39.3 @@ -114,7 +114,7 @@
    39.4    | tryres (th, []) = raise THM("tryres", 0, [th]);
    39.5  
    39.6  fun gen_make_elim elim_rls rl =
    39.7 -      Drule.standard (tryres (rl, elim_rls @ [revcut_rl]));
    39.8 +  Drule.export_without_context (tryres (rl, elim_rls @ [revcut_rl]));
    39.9  
   39.10  (*Turns iff rules into safe elimination rules*)
   39.11  fun mk_free_SEs iffs = map (gen_make_elim [@{thm conjE}, @{thm FalseE}]) (iffs RL [@{thm iffD1}]);