Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;

--- a/src/HOL/Tools/lin_arith.ML	Fri Feb 19 09:35:18 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Fri Feb 19 11:49:44 2010 +0100
@@ -6,7 +6,7 @@
 
 signature LIN_ARITH =
 sig
-  val pre_tac: Proof.context -> int -> tactic
+  val pre_tac: simpset -> int -> tactic
   val simple_tac: Proof.context -> int -> tactic
   val tac: Proof.context -> int -> tactic
   val simproc: simpset -> term -> thm option
@@ -705,13 +705,12 @@
     setmksimps (mksimps mksimps_pairs)
     addsimps [imp_conv_disj, iff_conv_conj_imp, de_Morgan_disj, de_Morgan_conj,
       not_all, not_ex, not_not]
-  fun prem_nnf_tac i st =
-    full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset)
-      i st
+  fun prem_nnf_tac ss = full_simp_tac (Simplifier.inherit_context ss nnf_simpset)
 in
 
-fun split_once_tac ctxt split_thms =
+fun split_once_tac ss split_thms =
   let
+    val ctxt = Simplifier.the_context ss
     val thy = ProofContext.theory_of ctxt
     val cond_split_tac = SUBGOAL (fn (subgoal, i) =>
       let
@@ -734,7 +733,7 @@
       REPEAT_DETERM o etac rev_mp,
       cond_split_tac,
       rtac ccontr,
-      prem_nnf_tac,
+      prem_nnf_tac ss,
       TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE))
     ]
   end;
@@ -746,15 +745,16 @@
 (* subgoals and finally attempt to solve them by finding an immediate        *)
 (* contradiction (i.e., a term and its negation) in their premises.          *)
 
-fun pre_tac ctxt i =
+fun pre_tac ss i =
 let
+  val ctxt = Simplifier.the_context ss;
   val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
   fun is_relevant t = is_some (decomp ctxt t)
 in
   DETERM (
     TRY (filter_prems_tac is_relevant i)
       THEN (
-        (TRY o REPEAT_ALL_NEW (split_once_tac ctxt split_thms))
+        (TRY o REPEAT_ALL_NEW (split_once_tac ss split_thms))
           THEN_ALL_NEW
             (CONVERSION Drule.beta_eta_conversion
               THEN'

--- a/src/HOL/ex/Arith_Examples.thy	Fri Feb 19 09:35:18 2010 +0100
+++ b/src/HOL/ex/Arith_Examples.thy	Fri Feb 19 11:49:44 2010 +0100
@@ -123,12 +123,12 @@
   (* FIXME: need to replace 1 by its numeral representation *)
   apply (subst numeral_1_eq_1 [symmetric])
   (* FIXME: arith does not know about iszero *)
-  apply (tactic {* Lin_Arith.pre_tac @{context} 1 *})
+  apply (tactic {* Lin_Arith.pre_tac @{simpset} 1 *})
 oops
 
 lemma "(i::int) mod 42 <= 41"
   (* FIXME: arith does not know about iszero *)
-  apply (tactic {* Lin_Arith.pre_tac @{context} 1 *})
+  apply (tactic {* Lin_Arith.pre_tac @{simpset} 1 *})
 oops
 
 lemma "-(i::int) * 1 = 0 ==> i = 0"

--- a/src/Provers/Arith/fast_lin_arith.ML	Fri Feb 19 09:35:18 2010 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Feb 19 11:49:44 2010 +0100
@@ -56,7 +56,7 @@
   val pre_decomp: Proof.context -> typ list * term list -> (typ list * term list) list
 
   (*preprocessing, performed on the goal -- must do the same as 'pre_decomp':*)
-  val pre_tac: Proof.context -> int -> tactic
+  val pre_tac: simpset -> int -> tactic
 
   (*the limit on the number of ~= allowed; because each ~= is split
     into two cases, this can lead to an explosion*)
@@ -792,7 +792,7 @@
       (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
       DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
       (* user-defined preprocessing of the subgoal *)
-      DETERM (LA_Data.pre_tac ctxt i) THEN
+      DETERM (LA_Data.pre_tac ss i) THEN
       PRIMITIVE (trace_thm ctxt "State after pre_tac:") THEN
       (* prove every resulting subgoal, using its justification *)
       EVERY (map just1 justs)