explicitly qualify Drule.standard;
authorwenzelm
Sat Oct 17 00:52:37 2009 +0200 (2009-10-17)
changeset 32957675c0c7e6a37
parent 32956 c39860141415
child 32958 3228627994d9
explicitly qualify Drule.standard;
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_rep_proofs.ML
src/HOL/Tools/Function/size.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/numeral_simprocs.ML
src/HOL/Tools/record.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
src/Provers/hypsubst.ML
src/Provers/typedsimp.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
src/ZF/int_arith.ML
     1.1 --- a/src/FOL/simpdata.ML	Fri Oct 16 10:55:07 2009 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Sat Oct 17 00:52:37 2009 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  
     1.5  (*Congruence rules for = or <-> (instead of ==)*)
     1.6  fun mk_meta_cong rl =
     1.7 -  standard(mk_meta_eq (mk_meta_prems rl))
     1.8 +  Drule.standard (mk_meta_eq (mk_meta_prems rl))
     1.9    handle THM _ =>
    1.10    error("Premises and conclusion of congruence rules must use =-equality or <->");
    1.11  
     2.1 --- a/src/FOLP/simp.ML	Fri Oct 16 10:55:07 2009 +0200
     2.2 +++ b/src/FOLP/simp.ML	Sat Oct 17 00:52:37 2009 +0200
     2.3 @@ -519,7 +519,7 @@
     2.4  (* Compute Congruence rules for individual constants using the substition
     2.5     rules *)
     2.6  
     2.7 -val subst_thms = map standard subst_thms;
     2.8 +val subst_thms = map Drule.standard subst_thms;
     2.9  
    2.10  
    2.11  fun exp_app(0,t) = t
     3.1 --- a/src/HOL/Import/hol4rews.ML	Fri Oct 16 10:55:07 2009 +0200
     3.2 +++ b/src/HOL/Import/hol4rews.ML	Sat Oct 17 00:52:37 2009 +0200
     3.3 @@ -386,7 +386,7 @@
     3.4      fun process ((bthy,bthm), hth as (_,thm)) thy =
     3.5        let
     3.6          val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm);
     3.7 -        val thm2 = standard thm1;
     3.8 +        val thm2 = Drule.standard thm1;
     3.9        in
    3.10          thy
    3.11          |> PureThy.store_thm (Binding.name bthm, thm2)
     4.1 --- a/src/HOL/Import/shuffler.ML	Fri Oct 16 10:55:07 2009 +0200
     4.2 +++ b/src/HOL/Import/shuffler.ML	Sat Oct 17 00:52:37 2009 +0200
     4.3 @@ -101,7 +101,7 @@
     4.4          val th4 = implies_elim_list (assume cPPQ) [th3,th3]
     4.5                                      |> implies_intr_list [cPPQ,cP]
     4.6      in
     4.7 -        equal_intr th4 th1 |> standard
     4.8 +        equal_intr th4 th1 |> Drule.standard
     4.9      end
    4.10  
    4.11  val imp_comm =
    4.12 @@ -121,7 +121,7 @@
    4.13          val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP]
    4.14                                      |> implies_intr_list [cQPR,cP,cQ]
    4.15      in
    4.16 -        equal_intr th1 th2 |> standard
    4.17 +        equal_intr th1 th2 |> Drule.standard
    4.18      end
    4.19  
    4.20  val def_norm =
    4.21 @@ -148,7 +148,7 @@
    4.22                                |> forall_intr cv
    4.23                                |> implies_intr cPQ
    4.24      in
    4.25 -        equal_intr th1 th2 |> standard
    4.26 +        equal_intr th1 th2 |> Drule.standard
    4.27      end
    4.28  
    4.29  val all_comm =
    4.30 @@ -174,7 +174,7 @@
    4.31                           |> forall_intr_list [cy,cx]
    4.32                           |> implies_intr cl
    4.33      in
    4.34 -        equal_intr th1 th2 |> standard
    4.35 +        equal_intr th1 th2 |> Drule.standard
    4.36      end
    4.37  
    4.38  val equiv_comm =
    4.39 @@ -188,7 +188,7 @@
    4.40          val th1  = assume ctu |> symmetric |> implies_intr ctu
    4.41          val th2  = assume cut |> symmetric |> implies_intr cut
    4.42      in
    4.43 -        equal_intr th1 th2 |> standard
    4.44 +        equal_intr th1 th2 |> Drule.standard
    4.45      end
    4.46  
    4.47  (* This simplification procedure rewrites !!x y. P x y
     5.1 --- a/src/HOL/Matrix/cplex/matrixlp.ML	Fri Oct 16 10:55:07 2009 +0200
     5.2 +++ b/src/HOL/Matrix/cplex/matrixlp.ML	Sat Oct 17 00:52:37 2009 +0200
     5.3 @@ -18,7 +18,7 @@
     5.4  
     5.5  fun inst_real thm =
     5.6    let val certT = ctyp_of (Thm.theory_of_thm thm) in
     5.7 -    standard (Thm.instantiate
     5.8 +    Drule.standard (Thm.instantiate
     5.9        ([(certT (TVar (hd (OldTerm.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
    5.10    end
    5.11  
    5.12 @@ -59,7 +59,7 @@
    5.13          val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
    5.14          val v = TVar (hd (sort ord (OldTerm.term_tvars (prop_of thm))))
    5.15      in
    5.16 -        standard (Thm.instantiate ([(certT v, certT ty)], []) thm)
    5.17 +        Drule.standard (Thm.instantiate ([(certT v, certT ty)], []) thm)
    5.18      end
    5.19  
    5.20  fun inst_tvars [] thms = thms
     6.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Oct 16 10:55:07 2009 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Oct 17 00:52:37 2009 +0200
     6.3 @@ -153,7 +153,7 @@
     6.4  
     6.5  fun projections rule =
     6.6    Project_Rule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
     6.7 -  |> map (standard #> RuleCases.save rule);
     6.8 +  |> map (Drule.standard #> RuleCases.save rule);
     6.9  
    6.10  val supp_prod = thm "supp_prod";
    6.11  val fresh_prod = thm "fresh_prod";
    6.12 @@ -313,7 +313,7 @@
    6.13  
    6.14      val unfolded_perm_eq_thms =
    6.15        if length descr = length new_type_names then []
    6.16 -      else map standard (List.drop (split_conj_thm
    6.17 +      else map Drule.standard (List.drop (split_conj_thm
    6.18          (Goal.prove_global thy2 [] []
    6.19            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    6.20              (map (fn (c as (s, T), x) =>
    6.21 @@ -333,7 +333,7 @@
    6.22  
    6.23      val perm_empty_thms = maps (fn a =>
    6.24        let val permT = mk_permT (Type (a, []))
    6.25 -      in map standard (List.take (split_conj_thm
    6.26 +      in map Drule.standard (List.take (split_conj_thm
    6.27          (Goal.prove_global thy2 [] []
    6.28            (augment_sort thy2 [pt_class_of thy2 a]
    6.29              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    6.30 @@ -365,7 +365,7 @@
    6.31          val pt_inst = pt_inst_of thy2 a;
    6.32          val pt2' = pt_inst RS pt2;
    6.33          val pt2_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
    6.34 -      in List.take (map standard (split_conj_thm
    6.35 +      in List.take (map Drule.standard (split_conj_thm
    6.36          (Goal.prove_global thy2 [] []
    6.37             (augment_sort thy2 [pt_class_of thy2 a]
    6.38               (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    6.39 @@ -400,7 +400,7 @@
    6.40          val pt3' = pt_inst RS pt3;
    6.41          val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
    6.42          val pt3_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
    6.43 -      in List.take (map standard (split_conj_thm
    6.44 +      in List.take (map Drule.standard (split_conj_thm
    6.45          (Goal.prove_global thy2 [] []
    6.46            (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
    6.47               (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
    6.48 @@ -585,7 +585,7 @@
    6.49        (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
    6.50        (perm_indnames ~~ descr);
    6.51  
    6.52 -    fun mk_perm_closed name = map (fn th => standard (th RS mp))
    6.53 +    fun mk_perm_closed name = map (fn th => Drule.standard (th RS mp))
    6.54        (List.take (split_conj_thm (Goal.prove_global thy4 [] []
    6.55          (augment_sort thy4
    6.56            (pt_class_of thy4 name :: map (cp_class_of thy4 name) (dt_atoms \ name))
    6.57 @@ -810,7 +810,7 @@
    6.58        let
    6.59          val rep_const = cterm_of thy
    6.60            (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
    6.61 -        val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    6.62 +        val dist = Drule.standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    6.63          val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
    6.64            ((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
    6.65        in
    6.66 @@ -874,7 +874,7 @@
    6.67            let
    6.68              val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
    6.69                simp_tac (global_simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
    6.70 -          in dist_thm :: standard (dist_thm RS not_sym) ::
    6.71 +          in dist_thm :: Drule.standard (dist_thm RS not_sym) ::
    6.72              prove_distinct_thms p (k, ts)
    6.73            end;
    6.74  
    6.75 @@ -1089,7 +1089,7 @@
    6.76  
    6.77      val finite_supp_thms = map (fn atom =>
    6.78        let val atomT = Type (atom, [])
    6.79 -      in map standard (List.take
    6.80 +      in map Drule.standard (List.take
    6.81          (split_conj_thm (Goal.prove_global thy8 [] []
    6.82             (augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort)
    6.83               (HOLogic.mk_Trueprop
    6.84 @@ -1535,7 +1535,7 @@
    6.85            in
    6.86              (R $ x $ y, R' $ mk_perm [] pi x $ mk_perm [] pi y)
    6.87            end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs));
    6.88 -        val ths = map (fn th => standard (th RS mp)) (split_conj_thm
    6.89 +        val ths = map (fn th => Drule.standard (th RS mp)) (split_conj_thm
    6.90            (Goal.prove_global thy11 [] []
    6.91              (augment_sort thy1 pt_cp_sort
    6.92                (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
    6.93 @@ -1567,7 +1567,7 @@
    6.94            (finite $ (Const ("Nominal.supp", T --> aset) $ f)))
    6.95              (rec_fns ~~ rec_fn_Ts)
    6.96        in
    6.97 -        map (fn th => standard (th RS mp)) (split_conj_thm
    6.98 +        map (fn th => Drule.standard (th RS mp)) (split_conj_thm
    6.99            (Goal.prove_global thy11 []
   6.100              (map (augment_sort thy11 fs_cp_sort) fins)
   6.101              (augment_sort thy11 fs_cp_sort
   6.102 @@ -1610,7 +1610,7 @@
   6.103              val y = Free ("y", U);
   6.104              val y' = Free ("y'", U)
   6.105            in
   6.106 -            standard (Goal.prove (ProofContext.init thy11) []
   6.107 +            Drule.standard (Goal.prove (ProofContext.init thy11) []
   6.108                (map (augment_sort thy11 fs_cp_sort)
   6.109                  (finite_prems @
   6.110                     [HOLogic.mk_Trueprop (R $ x $ y),
   6.111 @@ -2055,7 +2055,7 @@
   6.112           ((Binding.name "rec_equiv'", flat rec_equiv_thms'), []),
   6.113           ((Binding.name "rec_fin_supp", flat rec_fin_supp_thms), []),
   6.114           ((Binding.name "rec_fresh", flat rec_fresh_thms), []),
   6.115 -         ((Binding.name "rec_unique", map standard rec_unique_thms), []),
   6.116 +         ((Binding.name "rec_unique", map Drule.standard rec_unique_thms), []),
   6.117           ((Binding.name "recs", rec_thms), [])] ||>
   6.118        Sign.parent_path ||>
   6.119        map_nominal_datatypes (fold Symtab.update dt_infos);
     7.1 --- a/src/HOL/Statespace/state_fun.ML	Fri Oct 16 10:55:07 2009 +0200
     7.2 +++ b/src/HOL/Statespace/state_fun.ML	Sat Oct 17 00:52:37 2009 +0200
     7.3 @@ -316,7 +316,7 @@
     7.4                    val prop = list_all ([("n",nT),("x",eT)],
     7.5                                Logic.mk_equals (Const ("Ex",Tex)$Abs(s,T,eq),
     7.6                                                 HOLogic.true_const));
     7.7 -                  val thm = standard (prove prop);
     7.8 +                  val thm = Drule.standard (prove prop);
     7.9                    val thm' = if swap then swap_ex_eq OF [thm] else thm
    7.10               in SOME thm' end
    7.11               handle TERM _ => NONE)
     8.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Oct 16 10:55:07 2009 +0200
     8.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Sat Oct 17 00:52:37 2009 +0200
     8.3 @@ -244,8 +244,10 @@
     8.4          val _ $ (_ $ (cong_f $ _) $ _) = concl_of arg_cong;
     8.5          val rep_const = cterm_of thy
     8.6            (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> Univ_elT));
     8.7 -        val cong' = standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
     8.8 -        val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
     8.9 +        val cong' =
    8.10 +          Drule.standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
    8.11 +        val dist =
    8.12 +          Drule.standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    8.13          val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs))
    8.14            ((Sign.add_path tname thy, defs, [], 1), constrs ~~ constr_syntax)
    8.15        in
    8.16 @@ -520,7 +522,7 @@
    8.17                let
    8.18                  val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
    8.19                    EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
    8.20 -              in dist_thm :: standard (dist_thm RS not_sym) :: prove ts end;
    8.21 +              in dist_thm :: Drule.standard (dist_thm RS not_sym) :: prove ts end;
    8.22        in prove ts end;
    8.23  
    8.24      val distinct_thms = map2 (prove_distinct_thms)
     9.1 --- a/src/HOL/Tools/Function/size.ML	Fri Oct 16 10:55:07 2009 +0200
     9.2 +++ b/src/HOL/Tools/Function/size.ML	Sat Oct 17 00:52:37 2009 +0200
     9.3 @@ -198,7 +198,7 @@
     9.4  
     9.5      fun prove_size_eqs p size_fns size_ofp simpset =
     9.6        maps (fn (((_, (_, _, constrs)), size_const), T) =>
     9.7 -        map (fn constr => standard (SkipProof.prove ctxt [] []
     9.8 +        map (fn constr => Drule.standard (SkipProof.prove ctxt [] []
     9.9            (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
    9.10               size_ofp size_const T constr)
    9.11            (fn _ => simp_tac simpset 1))) constrs)
    10.1 --- a/src/HOL/Tools/TFL/post.ML	Fri Oct 16 10:55:07 2009 +0200
    10.2 +++ b/src/HOL/Tools/TFL/post.ML	Sat Oct 17 00:52:37 2009 +0200
    10.3 @@ -144,7 +144,7 @@
    10.4  
    10.5  (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
    10.6  val meta_outer =
    10.7 -  curry_rule o standard o
    10.8 +  curry_rule o Drule.standard o
    10.9    rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
   10.10  
   10.11  (*Strip off the outer !P*)
   10.12 @@ -166,7 +166,7 @@
   10.13                 {f = f, R = R, rules = rules,
   10.14                  full_pats_TCs = full_pats_TCs,
   10.15                  TCs = TCs}
   10.16 -       val rules' = map (standard o ObjectLogic.rulify_no_asm)
   10.17 +       val rules' = map (Drule.standard o ObjectLogic.rulify_no_asm)
   10.18                          (R.CONJUNCTS rules)
   10.19           in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
   10.20          rules = ListPair.zip(rules', rows),
   10.21 @@ -195,7 +195,7 @@
   10.22      | solve_eq (th, [a], i) = [(a, i)]
   10.23      | solve_eq (th, splitths as (_ :: _), i) = 
   10.24        (writeln "Proving unsplit equation...";
   10.25 -      [((standard o ObjectLogic.rulify_no_asm)
   10.26 +      [((Drule.standard o ObjectLogic.rulify_no_asm)
   10.27            (CaseSplit.splitto splitths th), i)])
   10.28        (* if there's an error, pretend nothing happened with this definition 
   10.29           We should probably print something out so that the user knows...? *)
   10.30 @@ -252,7 +252,7 @@
   10.31   in (theory,
   10.32       (*return the conjoined induction rule and recursion equations,
   10.33         with assumptions remaining to discharge*)
   10.34 -     standard (induction RS (rules RS conjI)))
   10.35 +     Drule.standard (induction RS (rules RS conjI)))
   10.36   end
   10.37  
   10.38  fun defer thy congs fid seqs =
    11.1 --- a/src/HOL/Tools/arith_data.ML	Fri Oct 16 10:55:07 2009 +0200
    11.2 +++ b/src/HOL/Tools/arith_data.ML	Sat Oct 17 00:52:37 2009 +0200
    11.3 @@ -77,7 +77,7 @@
    11.4  fun prove_conv tacs ctxt (_: thm list) = prove_conv_nohyps tacs ctxt;
    11.5  
    11.6  fun prove_conv2 expand_tac norm_tac ss tu = (*FIXME avoid standard*)
    11.7 -  mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
    11.8 +  mk_meta_eq (Drule.standard (Goal.prove (Simplifier.the_context ss) [] []
    11.9        (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
   11.10      (K (EVERY [expand_tac, norm_tac ss]))));
   11.11  
    12.1 --- a/src/HOL/Tools/choice_specification.ML	Fri Oct 16 10:55:07 2009 +0200
    12.2 +++ b/src/HOL/Tools/choice_specification.ML	Sat Oct 17 00:52:37 2009 +0200
    12.3 @@ -75,7 +75,7 @@
    12.4  fun add_specification axiomatic cos arg =
    12.5      arg |> apsnd Thm.freezeT
    12.6          |> proc_exprop axiomatic cos
    12.7 -        |> apsnd standard
    12.8 +        |> apsnd Drule.standard
    12.9  
   12.10  
   12.11  (* Collect all intances of constants in term *)
   12.12 @@ -188,7 +188,7 @@
   12.13                      in
   12.14                          args |> apsnd (remove_alls frees)
   12.15                               |> apsnd undo_imps
   12.16 -                             |> apsnd standard
   12.17 +                             |> apsnd Drule.standard
   12.18                               |> Thm.theory_attributes (map (Attrib.attribute thy) atts)
   12.19                               |> add_final
   12.20                               |> Library.swap
    13.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Oct 16 10:55:07 2009 +0200
    13.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sat Oct 17 00:52:37 2009 +0200
    13.3 @@ -477,7 +477,7 @@
    13.4        (fn NONE => "X" | SOME k' => string_of_int k')
    13.5          (ks @ [SOME k]))) arities));
    13.6  
    13.7 -fun prep_intrs intrs = map (rename_term o #prop o rep_thm o standard) intrs;
    13.8 +fun prep_intrs intrs = map (rename_term o #prop o rep_thm o Drule.standard) intrs;
    13.9  
   13.10  fun constrain cs [] = []
   13.11    | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs (s : string) of
    14.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Fri Oct 16 10:55:07 2009 +0200
    14.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Oct 17 00:52:37 2009 +0200
    14.3 @@ -210,7 +210,7 @@
    14.4  
    14.5  (*push the unary minus down: - x * y = x * - y *)
    14.6  val minus_mult_eq_1_to_2 =
    14.7 -    [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> standard;
    14.8 +    [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> Drule.standard;
    14.9  
   14.10  (*to extract again any uncancelled minuses*)
   14.11  val minus_from_mult_simps =
    15.1 --- a/src/HOL/Tools/record.ML	Fri Oct 16 10:55:07 2009 +0200
    15.2 +++ b/src/HOL/Tools/record.ML	Sat Oct 17 00:52:37 2009 +0200
    15.3 @@ -1045,7 +1045,7 @@
    15.4          we varify the proposition manually here.*)
    15.5    else
    15.6      let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac
    15.7 -    in if stndrd then standard prf else prf end;
    15.8 +    in if stndrd then Drule.standard prf else prf end;
    15.9  
   15.10  fun quick_and_dirty_prf noopt opt () =
   15.11    if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty
   15.12 @@ -1097,7 +1097,7 @@
   15.13            if is_sel_upd_pair thy acc upd
   15.14            then o_eq_dest
   15.15            else o_eq_id_dest;
   15.16 -      in standard (othm RS dest) end;
   15.17 +      in Drule.standard (othm RS dest) end;
   15.18    in map get_simp upd_funs end;
   15.19  
   15.20  fun get_updupd_simp thy defset intros_tac u u' comp =
   15.21 @@ -1118,7 +1118,7 @@
   15.22              REPEAT_DETERM (intros_tac 1),
   15.23              TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)]);
   15.24      val dest = if comp then o_eq_dest_lhs else o_eq_dest;
   15.25 -  in standard (othm RS dest) end;
   15.26 +  in Drule.standard (othm RS dest) end;
   15.27  
   15.28  fun get_updupd_simps thy term defset intros_tac =
   15.29    let
   15.30 @@ -1312,7 +1312,8 @@
   15.31              val ss = get_sel_upd_defs thy;
   15.32              val uathm = get_upd_acc_cong_thm upd acc thy ss;
   15.33            in
   15.34 -            [standard (uathm RS updacc_noopE), standard (uathm RS updacc_noop_compE)]
   15.35 +           [Drule.standard (uathm RS updacc_noopE),
   15.36 +            Drule.standard (uathm RS updacc_noop_compE)]
   15.37            end;
   15.38  
   15.39          (*If f is constant then (f o g) = f. we know that K_skeleton
   15.40 @@ -1755,7 +1756,7 @@
   15.41        to prove other theorems. We haven't given names to the accessors
   15.42        f, g etc yet however, so we generate an ext structure with
   15.43        free variables as all arguments and allow the introduction tactic to
   15.44 -      operate on it as far as it can. We then use standard to convert
   15.45 +      operate on it as far as it can. We then use Drule.standard to convert
   15.46        the free variables into unifiable variables and unify them with
   15.47        (roughly) the definition of the accessor.*)
   15.48      fun surject_prf () =
   15.49 @@ -1766,8 +1767,8 @@
   15.50            simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
   15.51            REPEAT_ALL_NEW intros_tac 1;
   15.52          val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
   15.53 -        val [halfway] = Seq.list_of (tactic1 start);    (* FIXME Seq.lift_of ?? *)
   15.54 -        val [surject] = Seq.list_of (tactic2 (standard halfway));    (* FIXME Seq.lift_of ?? *)
   15.55 +        val [halfway] = Seq.list_of (tactic1 start);  (* FIXME Seq.lift_of ?? *)
   15.56 +        val [surject] = Seq.list_of (tactic2 (Drule.standard halfway));  (* FIXME Seq.lift_of ?? *)
   15.57        in
   15.58          surject
   15.59        end;
   15.60 @@ -2168,14 +2169,14 @@
   15.61      fun sel_convs_prf () =
   15.62        map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props;
   15.63      val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
   15.64 -    fun sel_convs_standard_prf () = map standard sel_convs
   15.65 +    fun sel_convs_standard_prf () = map Drule.standard sel_convs
   15.66      val sel_convs_standard =
   15.67        timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
   15.68  
   15.69      fun upd_convs_prf () =
   15.70        map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props;
   15.71      val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
   15.72 -    fun upd_convs_standard_prf () = map standard upd_convs
   15.73 +    fun upd_convs_standard_prf () = map Drule.standard upd_convs
   15.74      val upd_convs_standard =
   15.75        timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
   15.76  
   15.77 @@ -2183,7 +2184,7 @@
   15.78        let
   15.79          val symdefs = map symmetric (sel_defs @ upd_defs);
   15.80          val fold_ss = HOL_basic_ss addsimps symdefs;
   15.81 -        val ua_congs = map (standard o simplify fold_ss) upd_acc_cong_assists;
   15.82 +        val ua_congs = map (Drule.standard o simplify fold_ss) upd_acc_cong_assists;
   15.83        in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
   15.84      val (fold_congs, unfold_congs) =
   15.85        timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
   15.86 @@ -2217,7 +2218,7 @@
   15.87              [(cterm_of defs_thy Pvar, cterm_of defs_thy
   15.88                (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
   15.89              induct_scheme;
   15.90 -        in standard (ObjectLogic.rulify (mp OF [ind, refl])) end;
   15.91 +        in Drule.standard (ObjectLogic.rulify (mp OF [ind, refl])) end;
   15.92  
   15.93      fun cases_scheme_prf_noopt () =
   15.94        prove_standard [] cases_scheme_prop
   15.95 @@ -2262,7 +2263,7 @@
   15.96              rtac (prop_subst OF [surjective]) 1,
   15.97              REPEAT (etac meta_allE 1), atac 1]);
   15.98      val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
   15.99 -    fun split_meta_standardise () = standard split_meta;
  15.100 +    fun split_meta_standardise () = Drule.standard split_meta;
  15.101      val split_meta_standard =
  15.102        timeit_msg "record split_meta standard:" split_meta_standardise;
  15.103  
  15.104 @@ -2287,7 +2288,7 @@
  15.105            |> equal_elim (symmetric split_meta') (*!!r. P r*)
  15.106            |> meta_to_obj_all                    (*All r. P r*)
  15.107            |> implies_intr cr                    (* 2 ==> 1 *)
  15.108 -     in standard (thr COMP (thl COMP iffI)) end;
  15.109 +     in Drule.standard (thr COMP (thl COMP iffI)) end;
  15.110  
  15.111      fun split_object_prf_noopt () =
  15.112        prove_standard [] split_object_prop
    16.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Oct 16 10:55:07 2009 +0200
    16.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Oct 17 00:52:37 2009 +0200
    16.3 @@ -168,7 +168,7 @@
    16.4  val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
    16.5  val abs_defin' = iso_locale RS iso_abs_defin';
    16.6  val rep_defin' = iso_locale RS iso_rep_defin';
    16.7 -val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
    16.8 +val iso_rews = map Drule.standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
    16.9  
   16.10  (* ----- generating beta reduction rules from definitions-------------------- *)
   16.11  
   16.12 @@ -251,7 +251,7 @@
   16.13    val exhaust = pg con_appls (mk_trp exh) (K tacs);
   16.14    val _ = trace " Proving casedist...";
   16.15    val casedist =
   16.16 -    standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
   16.17 +    Drule.standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
   16.18  end;
   16.19  
   16.20  local 
   16.21 @@ -542,7 +542,7 @@
   16.22          flat
   16.23            (ListPair.map (distinct c) ((map #1 cs),leqs)) @
   16.24          distincts cs;
   16.25 -  in map standard (distincts (cons ~~ distincts_le)) end;
   16.26 +  in map Drule.standard (distincts (cons ~~ distincts_le)) end;
   16.27  
   16.28  local 
   16.29    fun pgterm rel con args =
   16.30 @@ -738,7 +738,7 @@
   16.31          maps (eq_tacs ctxt) eqs;
   16.32      in pg copy_take_defs goal tacs end;
   16.33  in
   16.34 -  val take_rews = map standard
   16.35 +  val take_rews = map Drule.standard
   16.36      (atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps);
   16.37  end; (* local *)
   16.38  
    17.1 --- a/src/Provers/hypsubst.ML	Fri Oct 16 10:55:07 2009 +0200
    17.2 +++ b/src/Provers/hypsubst.ML	Sat Oct 17 00:52:37 2009 +0200
    17.3 @@ -165,7 +165,7 @@
    17.4  
    17.5  end;
    17.6  
    17.7 -val ssubst = standard (Data.sym RS Data.subst);
    17.8 +val ssubst = Drule.standard (Data.sym RS Data.subst);
    17.9  
   17.10  fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
   17.11    case try (Logic.strip_assums_hyp #> hd #>
    18.1 --- a/src/Provers/typedsimp.ML	Fri Oct 16 10:55:07 2009 +0200
    18.2 +++ b/src/Provers/typedsimp.ML	Sat Oct 17 00:52:37 2009 +0200
    18.3 @@ -43,11 +43,11 @@
    18.4  (*For simplifying both sides of an equation:
    18.5        [| a=c; b=c |] ==> b=a
    18.6    Can use resolve_tac [split_eqn] to prepare an equation for simplification. *)
    18.7 -val split_eqn = standard (sym RSN (2,trans) RS sym);
    18.8 +val split_eqn = Drule.standard (sym RSN (2,trans) RS sym);
    18.9  
   18.10  
   18.11  (*    [| a=b; b=c |] ==> reduce(a,c)  *)
   18.12 -val red_trans = standard (trans RS red_if_equal);
   18.13 +val red_trans = Drule.standard (trans RS red_if_equal);
   18.14  
   18.15  (*For REWRITE rule: Make a reduction rule for simplification, e.g.
   18.16    [| a: C(0); ... ; a=c: C(0) |] ==> rec(0,a,b) = c: C(0) *)
    19.1 --- a/src/Pure/old_goals.ML	Fri Oct 16 10:55:07 2009 +0200
    19.2 +++ b/src/Pure/old_goals.ML	Sat Oct 17 00:52:37 2009 +0200
    19.3 @@ -305,7 +305,7 @@
    19.4              val th = Goal.conclude ath
    19.5              val thy' = Thm.theory_of_thm th
    19.6              val {hyps, prop, ...} = Thm.rep_thm th
    19.7 -            val final_th = standard th
    19.8 +            val final_th = Drule.standard th
    19.9          in  if not check then final_th
   19.10              else if not (Theory.eq_thy(thy,thy')) then !result_error_fn state
   19.11                  ("Theory of proof state has changed!" ^
   19.12 @@ -512,7 +512,7 @@
   19.13              0 => thm
   19.14            | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
   19.15    in
   19.16 -    standard (implies_intr_list As
   19.17 +    Drule.standard (implies_intr_list As
   19.18        (check (Seq.pull (EVERY (f asms) (trivial B)))))
   19.19    end;
   19.20  
    20.1 --- a/src/Sequents/simpdata.ML	Fri Oct 16 10:55:07 2009 +0200
    20.2 +++ b/src/Sequents/simpdata.ML	Sat Oct 17 00:52:37 2009 +0200
    20.3 @@ -49,7 +49,7 @@
    20.4  
    20.5  (*Congruence rules for = or <-> (instead of ==)*)
    20.6  fun mk_meta_cong rl =
    20.7 -  standard(mk_meta_eq (mk_meta_prems rl))
    20.8 +  Drule.standard(mk_meta_eq (mk_meta_prems rl))
    20.9    handle THM _ =>
   20.10    error("Premises and conclusion of congruence rules must use =-equality or <->");
   20.11  
    21.1 --- a/src/ZF/Tools/datatype_package.ML	Fri Oct 16 10:55:07 2009 +0200
    21.2 +++ b/src/ZF/Tools/datatype_package.ML	Sat Oct 17 00:52:37 2009 +0200
    21.3 @@ -292,7 +292,7 @@
    21.4           rtac case_trans 1,
    21.5           REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]);
    21.6  
    21.7 -  val free_iffs = map standard (con_defs RL [@{thm def_swap_iff}]);
    21.8 +  val free_iffs = map Drule.standard (con_defs RL [@{thm def_swap_iff}]);
    21.9  
   21.10    val case_eqns = map prove_case_eqn (flat con_ty_lists ~~ case_args ~~ tl con_defs);
   21.11  
   21.12 @@ -338,7 +338,7 @@
   21.13    val constructors =
   21.14        map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
   21.15  
   21.16 -  val free_SEs = map standard (Ind_Syntax.mk_free_SEs free_iffs);
   21.17 +  val free_SEs = map Drule.standard (Ind_Syntax.mk_free_SEs free_iffs);
   21.18  
   21.19    val {intrs, elim, induct, mutual_induct, ...} = ind_result
   21.20  
    22.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Oct 16 10:55:07 2009 +0200
    22.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Oct 17 00:52:37 2009 +0200
    22.3 @@ -193,9 +193,9 @@
    22.4          [rtac (@{thm Collect_subset} RS @{thm bnd_monoI}) 1,
    22.5           REPEAT (ares_tac (@{thms basic_monos} @ monos) 1)]);
    22.6  
    22.7 -  val dom_subset = standard (big_rec_def RS Fp.subs);
    22.8 +  val dom_subset = Drule.standard (big_rec_def RS Fp.subs);
    22.9  
   22.10 -  val unfold = standard ([big_rec_def, bnd_mono] MRS Fp.Tarski);
   22.11 +  val unfold = Drule.standard ([big_rec_def, bnd_mono] MRS Fp.Tarski);
   22.12  
   22.13    (********)
   22.14    val dummy = writeln "  Proving the introduction rules...";
   22.15 @@ -205,7 +205,7 @@
   22.16    val Part_trans =
   22.17        case rec_names of
   22.18             [_] => asm_rl
   22.19 -         | _   => standard (@{thm Part_subset} RS @{thm subset_trans});
   22.20 +         | _   => Drule.standard (@{thm Part_subset} RS @{thm subset_trans});
   22.21  
   22.22    (*To type-check recursive occurrences of the inductive sets, possibly
   22.23      enclosed in some monotonic operator M.*)
   22.24 @@ -503,7 +503,7 @@
   22.25       val Const (@{const_name Trueprop}, _) $ (pred_var $ _) = concl_of induct0
   22.26  
   22.27       val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0)
   22.28 -                  |> standard
   22.29 +                  |> Drule.standard
   22.30       and mutual_induct = CP.remove_split mutual_induct_fsplit
   22.31  
   22.32       val ([induct', mutual_induct'], thy') =
   22.33 @@ -514,7 +514,7 @@
   22.34      in ((thy', induct'), mutual_induct')
   22.35      end;  (*of induction_rules*)
   22.36  
   22.37 -  val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
   22.38 +  val raw_induct = Drule.standard ([big_rec_def, bnd_mono] MRS Fp.induct)
   22.39  
   22.40    val ((thy2, induct), mutual_induct) =
   22.41      if not coind then induction_rules raw_induct thy1
    23.1 --- a/src/ZF/ind_syntax.ML	Fri Oct 16 10:55:07 2009 +0200
    23.2 +++ b/src/ZF/ind_syntax.ML	Sat Oct 17 00:52:37 2009 +0200
    23.3 @@ -115,7 +115,7 @@
    23.4    | tryres (th, []) = raise THM("tryres", 0, [th]);
    23.5  
    23.6  fun gen_make_elim elim_rls rl =
    23.7 -      standard (tryres (rl, elim_rls @ [revcut_rl]));
    23.8 +      Drule.standard (tryres (rl, elim_rls @ [revcut_rl]));
    23.9  
   23.10  (*Turns iff rules into safe elimination rules*)
   23.11  fun mk_free_SEs iffs = map (gen_make_elim [@{thm conjE}, @{thm FalseE}]) (iffs RL [@{thm iffD1}]);
    24.1 --- a/src/ZF/int_arith.ML	Fri Oct 16 10:55:07 2009 +0200
    24.2 +++ b/src/ZF/int_arith.ML	Sat Oct 17 00:52:37 2009 +0200
    24.3 @@ -112,7 +112,7 @@
    24.4  
    24.5  (*push the unary minus down: - x * y = x * - y *)
    24.6  val int_minus_mult_eq_1_to_2 =
    24.7 -    [@{thm zmult_zminus}, @{thm zmult_zminus_right} RS sym] MRS trans |> standard;
    24.8 +    [@{thm zmult_zminus}, @{thm zmult_zminus_right} RS sym] MRS trans |> Drule.standard;
    24.9  
   24.10  (*to extract again any uncancelled minuses*)
   24.11  val int_minus_from_mult_simps =