--- a/src/FOL/simpdata.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/FOL/simpdata.ML Sat Oct 17 00:52:37 2009 +0200
@@ -27,7 +27,7 @@
(*Congruence rules for = or <-> (instead of ==)*)
fun mk_meta_cong rl =
- standard(mk_meta_eq (mk_meta_prems rl))
+ Drule.standard (mk_meta_eq (mk_meta_prems rl))
handle THM _ =>
error("Premises and conclusion of congruence rules must use =-equality or <->");
--- a/src/FOLP/simp.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/FOLP/simp.ML Sat Oct 17 00:52:37 2009 +0200
@@ -519,7 +519,7 @@
(* Compute Congruence rules for individual constants using the substition
rules *)
-val subst_thms = map standard subst_thms;
+val subst_thms = map Drule.standard subst_thms;
fun exp_app(0,t) = t
--- a/src/HOL/Import/hol4rews.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Import/hol4rews.ML Sat Oct 17 00:52:37 2009 +0200
@@ -386,7 +386,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 = standard thm1;
+ val thm2 = Drule.standard thm1;
in
thy
|> PureThy.store_thm (Binding.name bthm, thm2)
--- a/src/HOL/Import/shuffler.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Import/shuffler.ML Sat Oct 17 00:52:37 2009 +0200
@@ -101,7 +101,7 @@
val th4 = implies_elim_list (assume cPPQ) [th3,th3]
|> implies_intr_list [cPPQ,cP]
in
- equal_intr th4 th1 |> standard
+ equal_intr th4 th1 |> Drule.standard
end
val imp_comm =
@@ -121,7 +121,7 @@
val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP]
|> implies_intr_list [cQPR,cP,cQ]
in
- equal_intr th1 th2 |> standard
+ equal_intr th1 th2 |> Drule.standard
end
val def_norm =
@@ -148,7 +148,7 @@
|> forall_intr cv
|> implies_intr cPQ
in
- equal_intr th1 th2 |> standard
+ equal_intr th1 th2 |> Drule.standard
end
val all_comm =
@@ -174,7 +174,7 @@
|> forall_intr_list [cy,cx]
|> implies_intr cl
in
- equal_intr th1 th2 |> standard
+ equal_intr th1 th2 |> Drule.standard
end
val equiv_comm =
@@ -188,7 +188,7 @@
val th1 = assume ctu |> symmetric |> implies_intr ctu
val th2 = assume cut |> symmetric |> implies_intr cut
in
- equal_intr th1 th2 |> standard
+ equal_intr th1 th2 |> Drule.standard
end
(* This simplification procedure rewrites !!x y. P x y
--- a/src/HOL/Matrix/cplex/matrixlp.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Matrix/cplex/matrixlp.ML Sat Oct 17 00:52:37 2009 +0200
@@ -18,7 +18,7 @@
fun inst_real thm =
let val certT = ctyp_of (Thm.theory_of_thm thm) in
- standard (Thm.instantiate
+ Drule.standard (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
- standard (Thm.instantiate ([(certT v, certT ty)], []) thm)
+ Drule.standard (Thm.instantiate ([(certT v, certT ty)], []) thm)
end
fun inst_tvars [] thms = thms
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Sat Oct 17 00:52:37 2009 +0200
@@ -153,7 +153,7 @@
fun projections rule =
Project_Rule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
- |> map (standard #> RuleCases.save rule);
+ |> map (Drule.standard #> RuleCases.save rule);
val supp_prod = thm "supp_prod";
val fresh_prod = thm "fresh_prod";
@@ -313,7 +313,7 @@
val unfolded_perm_eq_thms =
if length descr = length new_type_names then []
- else map standard (List.drop (split_conj_thm
+ else map Drule.standard (List.drop (split_conj_thm
(Goal.prove_global thy2 [] []
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
(map (fn (c as (s, T), x) =>
@@ -333,7 +333,7 @@
val perm_empty_thms = maps (fn a =>
let val permT = mk_permT (Type (a, []))
- in map standard (List.take (split_conj_thm
+ in map Drule.standard (List.take (split_conj_thm
(Goal.prove_global thy2 [] []
(augment_sort thy2 [pt_class_of thy2 a]
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
@@ -365,7 +365,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 standard (split_conj_thm
+ in List.take (map Drule.standard (split_conj_thm
(Goal.prove_global thy2 [] []
(augment_sort thy2 [pt_class_of thy2 a]
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
@@ -400,7 +400,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 standard (split_conj_thm
+ in List.take (map Drule.standard (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",
@@ -585,7 +585,7 @@
(fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
(perm_indnames ~~ descr);
- fun mk_perm_closed name = map (fn th => standard (th RS mp))
+ fun mk_perm_closed name = map (fn th => Drule.standard (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) (dt_atoms \ name))
@@ -810,7 +810,7 @@
let
val rep_const = cterm_of thy
(Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
- val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
+ val dist = Drule.standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
in
@@ -874,7 +874,7 @@
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 :: standard (dist_thm RS not_sym) ::
+ in dist_thm :: Drule.standard (dist_thm RS not_sym) ::
prove_distinct_thms p (k, ts)
end;
@@ -1089,7 +1089,7 @@
val finite_supp_thms = map (fn atom =>
let val atomT = Type (atom, [])
- in map standard (List.take
+ in map Drule.standard (List.take
(split_conj_thm (Goal.prove_global thy8 [] []
(augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort)
(HOLogic.mk_Trueprop
@@ -1535,7 +1535,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 => standard (th RS mp)) (split_conj_thm
+ val ths = map (fn th => Drule.standard (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))))
@@ -1567,7 +1567,7 @@
(finite $ (Const ("Nominal.supp", T --> aset) $ f)))
(rec_fns ~~ rec_fn_Ts)
in
- map (fn th => standard (th RS mp)) (split_conj_thm
+ map (fn th => Drule.standard (th RS mp)) (split_conj_thm
(Goal.prove_global thy11 []
(map (augment_sort thy11 fs_cp_sort) fins)
(augment_sort thy11 fs_cp_sort
@@ -1610,7 +1610,7 @@
val y = Free ("y", U);
val y' = Free ("y'", U)
in
- standard (Goal.prove (ProofContext.init thy11) []
+ Drule.standard (Goal.prove (ProofContext.init thy11) []
(map (augment_sort thy11 fs_cp_sort)
(finite_prems @
[HOLogic.mk_Trueprop (R $ x $ y),
@@ -2055,7 +2055,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 standard rec_unique_thms), []),
+ ((Binding.name "rec_unique", map Drule.standard rec_unique_thms), []),
((Binding.name "recs", rec_thms), [])] ||>
Sign.parent_path ||>
map_nominal_datatypes (fold Symtab.update dt_infos);
--- a/src/HOL/Statespace/state_fun.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Statespace/state_fun.ML Sat Oct 17 00:52:37 2009 +0200
@@ -316,7 +316,7 @@
val prop = list_all ([("n",nT),("x",eT)],
Logic.mk_equals (Const ("Ex",Tex)$Abs(s,T,eq),
HOLogic.true_const));
- val thm = standard (prove prop);
+ val thm = Drule.standard (prove prop);
val thm' = if swap then swap_ex_eq OF [thm] else thm
in SOME thm' end
handle TERM _ => NONE)
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Sat Oct 17 00:52:37 2009 +0200
@@ -244,8 +244,10 @@
val _ $ (_ $ (cong_f $ _) $ _) = concl_of arg_cong;
val rep_const = cterm_of thy
(Const (Sign.intern_const thy ("Rep_" ^ tname), T --> Univ_elT));
- val cong' = standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
- val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
+ val cong' =
+ Drule.standard (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);
val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs))
((Sign.add_path tname thy, defs, [], 1), constrs ~~ constr_syntax)
in
@@ -520,7 +522,7 @@
let
val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
- in dist_thm :: standard (dist_thm RS not_sym) :: prove ts end;
+ in dist_thm :: Drule.standard (dist_thm RS not_sym) :: prove ts end;
in prove ts end;
val distinct_thms = map2 (prove_distinct_thms)
--- a/src/HOL/Tools/Function/size.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Tools/Function/size.ML Sat Oct 17 00:52:37 2009 +0200
@@ -198,7 +198,7 @@
fun prove_size_eqs p size_fns size_ofp simpset =
maps (fn (((_, (_, _, constrs)), size_const), T) =>
- map (fn constr => standard (SkipProof.prove ctxt [] []
+ map (fn constr => Drule.standard (SkipProof.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)
--- a/src/HOL/Tools/TFL/post.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Tools/TFL/post.ML Sat Oct 17 00:52:37 2009 +0200
@@ -144,7 +144,7 @@
(*lcp: put a theorem into Isabelle form, using meta-level connectives*)
val meta_outer =
- curry_rule o standard o
+ curry_rule o Drule.standard o
rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
(*Strip off the outer !P*)
@@ -166,7 +166,7 @@
{f = f, R = R, rules = rules,
full_pats_TCs = full_pats_TCs,
TCs = TCs}
- val rules' = map (standard o ObjectLogic.rulify_no_asm)
+ val rules' = map (Drule.standard o ObjectLogic.rulify_no_asm)
(R.CONJUNCTS rules)
in {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
rules = ListPair.zip(rules', rows),
@@ -195,7 +195,7 @@
| solve_eq (th, [a], i) = [(a, i)]
| solve_eq (th, splitths as (_ :: _), i) =
(writeln "Proving unsplit equation...";
- [((standard o ObjectLogic.rulify_no_asm)
+ [((Drule.standard 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...? *)
@@ -252,7 +252,7 @@
in (theory,
(*return the conjoined induction rule and recursion equations,
with assumptions remaining to discharge*)
- standard (induction RS (rules RS conjI)))
+ Drule.standard (induction RS (rules RS conjI)))
end
fun defer thy congs fid seqs =
--- a/src/HOL/Tools/arith_data.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Tools/arith_data.ML Sat Oct 17 00:52:37 2009 +0200
@@ -77,7 +77,7 @@
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 (standard (Goal.prove (Simplifier.the_context ss) [] []
+ mk_meta_eq (Drule.standard (Goal.prove (Simplifier.the_context ss) [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
(K (EVERY [expand_tac, norm_tac ss]))));
--- a/src/HOL/Tools/choice_specification.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Tools/choice_specification.ML Sat Oct 17 00:52:37 2009 +0200
@@ -75,7 +75,7 @@
fun add_specification axiomatic cos arg =
arg |> apsnd Thm.freezeT
|> proc_exprop axiomatic cos
- |> apsnd standard
+ |> apsnd Drule.standard
(* Collect all intances of constants in term *)
@@ -188,7 +188,7 @@
in
args |> apsnd (remove_alls frees)
|> apsnd undo_imps
- |> apsnd standard
+ |> apsnd Drule.standard
|> Thm.theory_attributes (map (Attrib.attribute thy) atts)
|> add_final
|> Library.swap
--- a/src/HOL/Tools/inductive_codegen.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Sat Oct 17 00:52:37 2009 +0200
@@ -477,7 +477,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 standard) intrs;
+fun prep_intrs intrs = map (rename_term o #prop o rep_thm o Drule.standard) intrs;
fun constrain cs [] = []
| constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs (s : string) of
--- a/src/HOL/Tools/numeral_simprocs.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Sat Oct 17 00:52:37 2009 +0200
@@ -210,7 +210,7 @@
(*push the unary minus down: - x * y = x * - y *)
val minus_mult_eq_1_to_2 =
- [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> standard;
+ [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> Drule.standard;
(*to extract again any uncancelled minuses*)
val minus_from_mult_simps =
--- a/src/HOL/Tools/record.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Tools/record.ML Sat Oct 17 00:52:37 2009 +0200
@@ -1045,7 +1045,7 @@
we varify the proposition manually here.*)
else
let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac
- in if stndrd then standard prf else prf end;
+ in if stndrd then Drule.standard prf else prf end;
fun quick_and_dirty_prf noopt opt () =
if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty
@@ -1097,7 +1097,7 @@
if is_sel_upd_pair thy acc upd
then o_eq_dest
else o_eq_id_dest;
- in standard (othm RS dest) end;
+ in Drule.standard (othm RS dest) end;
in map get_simp upd_funs end;
fun get_updupd_simp thy defset intros_tac u u' comp =
@@ -1118,7 +1118,7 @@
REPEAT_DETERM (intros_tac 1),
TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)]);
val dest = if comp then o_eq_dest_lhs else o_eq_dest;
- in standard (othm RS dest) end;
+ in Drule.standard (othm RS dest) end;
fun get_updupd_simps thy term defset intros_tac =
let
@@ -1312,7 +1312,8 @@
val ss = get_sel_upd_defs thy;
val uathm = get_upd_acc_cong_thm upd acc thy ss;
in
- [standard (uathm RS updacc_noopE), standard (uathm RS updacc_noop_compE)]
+ [Drule.standard (uathm RS updacc_noopE),
+ Drule.standard (uathm RS updacc_noop_compE)]
end;
(*If f is constant then (f o g) = f. we know that K_skeleton
@@ -1755,7 +1756,7 @@
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 standard to convert
+ 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
(roughly) the definition of the accessor.*)
fun surject_prf () =
@@ -1766,8 +1767,8 @@
simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
REPEAT_ALL_NEW intros_tac 1;
val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
- val [halfway] = Seq.list_of (tactic1 start); (* FIXME Seq.lift_of ?? *)
- val [surject] = Seq.list_of (tactic2 (standard halfway)); (* FIXME Seq.lift_of ?? *)
+ val [halfway] = Seq.list_of (tactic1 start); (* FIXME Seq.lift_of ?? *)
+ val [surject] = Seq.list_of (tactic2 (Drule.standard halfway)); (* FIXME Seq.lift_of ?? *)
in
surject
end;
@@ -2168,14 +2169,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 standard sel_convs
+ fun sel_convs_standard_prf () = map Drule.standard 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 standard upd_convs
+ fun upd_convs_standard_prf () = map Drule.standard upd_convs
val upd_convs_standard =
timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
@@ -2183,7 +2184,7 @@
let
val symdefs = map symmetric (sel_defs @ upd_defs);
val fold_ss = HOL_basic_ss addsimps symdefs;
- val ua_congs = map (standard o simplify fold_ss) upd_acc_cong_assists;
+ val ua_congs = map (Drule.standard 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;
@@ -2217,7 +2218,7 @@
[(cterm_of defs_thy Pvar, cterm_of defs_thy
(lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
induct_scheme;
- in standard (ObjectLogic.rulify (mp OF [ind, refl])) end;
+ in Drule.standard (ObjectLogic.rulify (mp OF [ind, refl])) end;
fun cases_scheme_prf_noopt () =
prove_standard [] cases_scheme_prop
@@ -2262,7 +2263,7 @@
rtac (prop_subst OF [surjective]) 1,
REPEAT (etac meta_allE 1), atac 1]);
val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
- fun split_meta_standardise () = standard split_meta;
+ fun split_meta_standardise () = Drule.standard split_meta;
val split_meta_standard =
timeit_msg "record split_meta standard:" split_meta_standardise;
@@ -2287,7 +2288,7 @@
|> equal_elim (symmetric split_meta') (*!!r. P r*)
|> meta_to_obj_all (*All r. P r*)
|> implies_intr cr (* 2 ==> 1 *)
- in standard (thr COMP (thl COMP iffI)) end;
+ in Drule.standard (thr COMP (thl COMP iffI)) end;
fun split_object_prf_noopt () =
prove_standard [] split_object_prop
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Oct 17 00:52:37 2009 +0200
@@ -168,7 +168,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 standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
+val iso_rews = map Drule.standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
(* ----- generating beta reduction rules from definitions-------------------- *)
@@ -251,7 +251,7 @@
val exhaust = pg con_appls (mk_trp exh) (K tacs);
val _ = trace " Proving casedist...";
val casedist =
- standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
+ Drule.standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
end;
local
@@ -542,7 +542,7 @@
flat
(ListPair.map (distinct c) ((map #1 cs),leqs)) @
distincts cs;
- in map standard (distincts (cons ~~ distincts_le)) end;
+ in map Drule.standard (distincts (cons ~~ distincts_le)) end;
local
fun pgterm rel con args =
@@ -738,7 +738,7 @@
maps (eq_tacs ctxt) eqs;
in pg copy_take_defs goal tacs end;
in
- val take_rews = map standard
+ val take_rews = map Drule.standard
(atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps);
end; (* local *)
--- a/src/Provers/hypsubst.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/Provers/hypsubst.ML Sat Oct 17 00:52:37 2009 +0200
@@ -165,7 +165,7 @@
end;
-val ssubst = standard (Data.sym RS Data.subst);
+val ssubst = Drule.standard (Data.sym RS Data.subst);
fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
case try (Logic.strip_assums_hyp #> hd #>
--- a/src/Provers/typedsimp.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/Provers/typedsimp.ML Sat Oct 17 00:52:37 2009 +0200
@@ -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 = standard (sym RSN (2,trans) RS sym);
+val split_eqn = Drule.standard (sym RSN (2,trans) RS sym);
(* [| a=b; b=c |] ==> reduce(a,c) *)
-val red_trans = standard (trans RS red_if_equal);
+val red_trans = Drule.standard (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) *)
--- a/src/Pure/old_goals.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/Pure/old_goals.ML Sat Oct 17 00:52:37 2009 +0200
@@ -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 = standard th
+ val final_th = Drule.standard 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
- standard (implies_intr_list As
+ Drule.standard (implies_intr_list As
(check (Seq.pull (EVERY (f asms) (trivial B)))))
end;
--- a/src/Sequents/simpdata.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/Sequents/simpdata.ML Sat Oct 17 00:52:37 2009 +0200
@@ -49,7 +49,7 @@
(*Congruence rules for = or <-> (instead of ==)*)
fun mk_meta_cong rl =
- standard(mk_meta_eq (mk_meta_prems rl))
+ Drule.standard(mk_meta_eq (mk_meta_prems rl))
handle THM _ =>
error("Premises and conclusion of congruence rules must use =-equality or <->");
--- a/src/ZF/Tools/datatype_package.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/ZF/Tools/datatype_package.ML Sat Oct 17 00:52:37 2009 +0200
@@ -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 standard (con_defs RL [@{thm def_swap_iff}]);
+ val free_iffs = map Drule.standard (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 standard (Ind_Syntax.mk_free_SEs free_iffs);
+ val free_SEs = map Drule.standard (Ind_Syntax.mk_free_SEs free_iffs);
val {intrs, elim, induct, mutual_induct, ...} = ind_result
--- a/src/ZF/Tools/inductive_package.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/ZF/Tools/inductive_package.ML Sat Oct 17 00:52:37 2009 +0200
@@ -193,9 +193,9 @@
[rtac (@{thm Collect_subset} RS @{thm bnd_monoI}) 1,
REPEAT (ares_tac (@{thms basic_monos} @ monos) 1)]);
- val dom_subset = standard (big_rec_def RS Fp.subs);
+ val dom_subset = Drule.standard (big_rec_def RS Fp.subs);
- val unfold = standard ([big_rec_def, bnd_mono] MRS Fp.Tarski);
+ val unfold = Drule.standard ([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
- | _ => standard (@{thm Part_subset} RS @{thm subset_trans});
+ | _ => Drule.standard (@{thm Part_subset} RS @{thm subset_trans});
(*To type-check recursive occurrences of the inductive sets, possibly
enclosed in some monotonic operator M.*)
@@ -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)
- |> standard
+ |> Drule.standard
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 = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
+ val raw_induct = Drule.standard ([big_rec_def, bnd_mono] MRS Fp.induct)
val ((thy2, induct), mutual_induct) =
if not coind then induction_rules raw_induct thy1
--- a/src/ZF/ind_syntax.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/ZF/ind_syntax.ML Sat Oct 17 00:52:37 2009 +0200
@@ -115,7 +115,7 @@
| tryres (th, []) = raise THM("tryres", 0, [th]);
fun gen_make_elim elim_rls rl =
- standard (tryres (rl, elim_rls @ [revcut_rl]));
+ Drule.standard (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}]);
--- a/src/ZF/int_arith.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/ZF/int_arith.ML Sat Oct 17 00:52:37 2009 +0200
@@ -112,7 +112,7 @@
(*push the unary minus down: - x * y = x * - y *)
val int_minus_mult_eq_1_to_2 =
- [@{thm zmult_zminus}, @{thm zmult_zminus_right} RS sym] MRS trans |> standard;
+ [@{thm zmult_zminus}, @{thm zmult_zminus_right} RS sym] MRS trans |> Drule.standard;
(*to extract again any uncancelled minuses*)
val int_minus_from_mult_simps =