# HG changeset patch # User wenzelm # Date 1255733557 -7200 # Node ID 675c0c7e6a37a88b1b813c8cd1ce3ae1e2eb059a # Parent c39860141415ecf8102f377eba5f37788a2c0d1d explicitly qualify Drule.standard; diff -r c39860141415 -r 675c0c7e6a37 src/FOL/simpdata.ML --- 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 <->"); diff -r c39860141415 -r 675c0c7e6a37 src/FOLP/simp.ML --- 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 diff -r c39860141415 -r 675c0c7e6a37 src/HOL/Import/hol4rews.ML --- 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) diff -r c39860141415 -r 675c0c7e6a37 src/HOL/Import/shuffler.ML --- 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 diff -r c39860141415 -r 675c0c7e6a37 src/HOL/Matrix/cplex/matrixlp.ML --- 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 diff -r c39860141415 -r 675c0c7e6a37 src/HOL/Nominal/nominal_datatype.ML --- 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); diff -r c39860141415 -r 675c0c7e6a37 src/HOL/Statespace/state_fun.ML --- 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) diff -r c39860141415 -r 675c0c7e6a37 src/HOL/Tools/Datatype/datatype_rep_proofs.ML --- 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) diff -r c39860141415 -r 675c0c7e6a37 src/HOL/Tools/Function/size.ML --- 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) diff -r c39860141415 -r 675c0c7e6a37 src/HOL/Tools/TFL/post.ML --- 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 = diff -r c39860141415 -r 675c0c7e6a37 src/HOL/Tools/arith_data.ML --- 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])))); diff -r c39860141415 -r 675c0c7e6a37 src/HOL/Tools/choice_specification.ML --- 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 diff -r c39860141415 -r 675c0c7e6a37 src/HOL/Tools/inductive_codegen.ML --- 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 diff -r c39860141415 -r 675c0c7e6a37 src/HOL/Tools/numeral_simprocs.ML --- 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 = diff -r c39860141415 -r 675c0c7e6a37 src/HOL/Tools/record.ML --- 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 diff -r c39860141415 -r 675c0c7e6a37 src/HOLCF/Tools/Domain/domain_theorems.ML --- 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 *) diff -r c39860141415 -r 675c0c7e6a37 src/Provers/hypsubst.ML --- 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 #> diff -r c39860141415 -r 675c0c7e6a37 src/Provers/typedsimp.ML --- 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) *) diff -r c39860141415 -r 675c0c7e6a37 src/Pure/old_goals.ML --- 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; diff -r c39860141415 -r 675c0c7e6a37 src/Sequents/simpdata.ML --- 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 <->"); diff -r c39860141415 -r 675c0c7e6a37 src/ZF/Tools/datatype_package.ML --- 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 diff -r c39860141415 -r 675c0c7e6a37 src/ZF/Tools/inductive_package.ML --- 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 diff -r c39860141415 -r 675c0c7e6a37 src/ZF/ind_syntax.ML --- 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}]); diff -r c39860141415 -r 675c0c7e6a37 src/ZF/int_arith.ML --- 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 =