--- a/src/Provers/hypsubst.ML Tue Apr 16 17:54:14 2013 +0200
+++ b/src/Provers/hypsubst.ML Thu Apr 18 17:07:01 2013 +0200
@@ -48,7 +48,7 @@
sig
val bound_hyp_subst_tac : int -> tactic
val hyp_subst_tac : int -> tactic
- val hyp_subst_tac' : simpset -> int -> tactic
+ val hyp_subst_tac' : Proof.context -> int -> tactic
val blast_hyp_subst_tac : bool -> int -> tactic
val stac : thm -> int -> tactic
val hypsubst_setup : theory -> theory
@@ -127,15 +127,16 @@
(*Select a suitable equality assumption; substitute throughout the subgoal
If bnd is true, then it replaces Bound variables only. *)
- fun gen_hyp_subst_tac opt_ss bnd =
+ fun gen_hyp_subst_tac opt_ctxt bnd =
let fun tac i st = SUBGOAL (fn (Bi, _) =>
let
val (k, _) = eq_var bnd true Bi
- val map_simpset = case opt_ss of
- NONE => Simplifier.global_context (Thm.theory_of_thm st)
- | SOME ss => Simplifier.inherit_context ss
- val hyp_subst_ss = map_simpset empty_ss |> Simplifier.set_mksimps (K (mk_eqs bnd))
- in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
+ val ctxt =
+ (case opt_ctxt of
+ NONE => Proof_Context.init_global (Thm.theory_of_thm st)
+ | SOME ctxt => ctxt)
+ val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd))
+ in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i,
etac thin_rl i, rotate_tac (~k) i]
end handle THM _ => no_tac | EQ_VAR => no_tac) i st
in REPEAT_DETERM1 o tac end;
@@ -200,8 +201,8 @@
val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
gen_hyp_subst_tac NONE false, vars_gen_hyp_subst_tac false];
-fun hyp_subst_tac' ss = FIRST' [ematch_tac [Data.thin_refl],
- gen_hyp_subst_tac (SOME ss) false, vars_gen_hyp_subst_tac false];
+fun hyp_subst_tac' ctxt = FIRST' [ematch_tac [Data.thin_refl],
+ gen_hyp_subst_tac (SOME ctxt) false, vars_gen_hyp_subst_tac false];
(*Substitutes for Bound variables only -- this is always safe*)
val bound_hyp_subst_tac =