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