--- a/src/FOL/simpdata.ML Fri Apr 30 17:18:29 2010 +0200
+++ b/src/FOL/simpdata.ML Fri Apr 30 18:06:29 2010 +0200
@@ -21,13 +21,13 @@
| _ => th RS @{thm iff_reflection_T};
(*Replace premises x=y, X<->Y by X==Y*)
-val mk_meta_prems =
- rule_by_tactic
+fun mk_meta_prems ctxt =
+ rule_by_tactic ctxt
(REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
(*Congruence rules for = or <-> (instead of ==)*)
-fun mk_meta_cong (_: simpset) rl =
- Drule.export_without_context (mk_meta_eq (mk_meta_prems rl))
+fun mk_meta_cong ss rl =
+ Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
handle THM _ =>
error("Premises and conclusion of congruence rules must use =-equality or <->");
--- a/src/HOL/Tools/TFL/post.ML Fri Apr 30 17:18:29 2010 +0200
+++ b/src/HOL/Tools/TFL/post.ML Fri Apr 30 18:06:29 2010 +0200
@@ -128,9 +128,9 @@
Split_Rule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl;
(*lcp: put a theorem into Isabelle form, using meta-level connectives*)
-val meta_outer =
+fun meta_outer ctxt =
curry_rule o Drule.export_without_context o
- rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
+ rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
(*Strip off the outer !P*)
val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
@@ -139,7 +139,9 @@
| tracing false msg = writeln msg;
fun simplify_defn strict thy cs ss congs wfs id pats def0 =
- let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
+ let
+ val ctxt = ProofContext.init thy
+ val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
val {rules,rows,TCs,full_pats_TCs} =
Prim.post_definition congs (thy, (def,pats))
val {lhs=f,rhs} = S.dest_eq (concl def)
@@ -153,7 +155,7 @@
TCs = TCs}
val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
(R.CONJUNCTS rules)
- in {induct = meta_outer (Object_Logic.rulify_no_asm (induction RS spec')),
+ in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm (induction RS spec')),
rules = ListPair.zip(rules', rows),
tcs = (termination_goals rules') @ tcs}
end
--- a/src/HOL/Tools/inductive.ML Fri Apr 30 17:18:29 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Fri Apr 30 18:06:29 2010 +0200
@@ -446,7 +446,7 @@
val cprop = Thm.cterm_of thy prop;
val tac = ALLGOALS (simp_case_tac ss) THEN prune_params_tac;
fun mk_elim rl =
- Thm.implies_intr cprop (Tactic.rule_by_tactic tac (Thm.assume cprop RS rl))
+ Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
|> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
in
(case get_first (try mk_elim) elims of
--- a/src/HOL/Tools/split_rule.ML Fri Apr 30 17:18:29 2010 +0200
+++ b/src/HOL/Tools/split_rule.ML Fri Apr 30 18:06:29 2010 +0200
@@ -116,7 +116,7 @@
fun split_rule_goal ctxt xss rl =
let
- fun one_split i s = Tactic.rule_by_tactic (pair_tac ctxt s i);
+ fun one_split i s = Tactic.rule_by_tactic ctxt (pair_tac ctxt s i);
fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
in
rl
--- a/src/Provers/classical.ML Fri Apr 30 17:18:29 2010 +0200
+++ b/src/Provers/classical.ML Fri Apr 30 18:06:29 2010 +0200
@@ -208,8 +208,11 @@
fun dup_intr th = zero_var_indexes (th RS classical);
fun dup_elim th =
- rule_by_tactic (TRYALL (etac revcut_rl))
- ((th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd);
+ let
+ val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
+ val ctxt = ProofContext.init (Thm.theory_of_thm rl);
+ in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
+
(**** Classical rule sets ****)
--- a/src/Pure/tactic.ML Fri Apr 30 17:18:29 2010 +0200
+++ b/src/Pure/tactic.ML Fri Apr 30 18:06:29 2010 +0200
@@ -7,7 +7,7 @@
signature BASIC_TACTIC =
sig
val trace_goalno_tac: (int -> tactic) -> int -> tactic
- val rule_by_tactic: tactic -> thm -> thm
+ val rule_by_tactic: Proof.context -> tactic -> thm -> thm
val assume_tac: int -> tactic
val eq_assume_tac: int -> tactic
val compose_tac: (bool * thm * int) -> int -> tactic
@@ -86,14 +86,14 @@
Seq.make(fn()=> seqcell));
(*Makes a rule by applying a tactic to an existing rule*)
-fun rule_by_tactic tac rl =
+fun rule_by_tactic ctxt tac rl =
let
- val ctxt = Variable.thm_context rl;
- val ((_, [st]), ctxt') = Variable.import true [rl] ctxt;
+ val ctxt' = Variable.declare_thm rl ctxt;
+ val ((_, [st]), ctxt'') = Variable.import true [rl] ctxt';
in
(case Seq.pull (tac st) of
NONE => raise THM ("rule_by_tactic", 0, [rl])
- | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st'))
+ | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt'' ctxt') st'))
end;
--- a/src/Sequents/simpdata.ML Fri Apr 30 17:18:29 2010 +0200
+++ b/src/Sequents/simpdata.ML Fri Apr 30 18:06:29 2010 +0200
@@ -42,13 +42,13 @@
Display.string_of_thm_without_context th));
(*Replace premises x=y, X<->Y by X==Y*)
-val mk_meta_prems =
- rule_by_tactic
+fun mk_meta_prems ctxt =
+ rule_by_tactic ctxt
(REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
(*Congruence rules for = or <-> (instead of ==)*)
-fun mk_meta_cong (_: simpset) rl =
- Drule.export_without_context(mk_meta_eq (mk_meta_prems rl))
+fun mk_meta_cong ss rl =
+ Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
handle THM _ =>
error("Premises and conclusion of congruence rules must use =-equality or <->");
--- a/src/ZF/Tools/inductive_package.ML Fri Apr 30 17:18:29 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML Fri Apr 30 18:06:29 2010 +0200
@@ -261,7 +261,7 @@
THEN (PRIMITIVE (fold_rule part_rec_defs));
(*Elimination*)
- val elim = rule_by_tactic basic_elim_tac
+ val elim = rule_by_tactic (ProofContext.init thy1) basic_elim_tac
(unfold RS Ind_Syntax.equals_CollectD)
(*Applies freeness of the given constructors, which *must* be unfolded by
@@ -269,7 +269,7 @@
con_defs=[] for inference systems.
Proposition A should have the form t:Si where Si is an inductive set*)
fun make_cases ctxt A =
- rule_by_tactic
+ rule_by_tactic ctxt
(basic_elim_tac THEN ALLGOALS (asm_full_simp_tac (simpset_of ctxt)) THEN basic_elim_tac)
(Thm.assume A RS elim)
|> Drule.export_without_context_open;