modernized some simproc setup;

--- a/src/HOL/Int.thy	Wed Jun 29 17:35:46 2011 +0200
+++ b/src/HOL/Int.thy	Wed Jun 29 18:12:34 2011 +0200
@@ -1545,9 +1545,13 @@
   of_int_0 of_int_1 of_int_add of_int_mult
 
 use "Tools/int_arith.ML"
-setup {* Int_Arith.global_setup *}
 declaration {* K Int_Arith.setup *}
 
+simproc_setup fast_arith ("(m::'a::{linordered_idom,number_ring}) < n" |
+  "(m::'a::{linordered_idom,number_ring}) <= n" |
+  "(m::'a::{linordered_idom,number_ring}) = n") =
+  {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
+
 setup {*
   Reorient_Proc.add
     (fn Const (@{const_name number_of}, _) $ _ => true | _ => false)

--- a/src/HOL/NSA/HyperDef.thy	Wed Jun 29 17:35:46 2011 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Wed Jun 29 18:12:34 2011 +0200
@@ -348,12 +348,12 @@
   #> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
       @{thm star_of_number_of}, @{thm star_of_add}, @{thm star_of_minus},
       @{thm star_of_diff}, @{thm star_of_mult}]
-  #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"})
-  #> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc_global @{theory}
-      "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
-      (K Lin_Arith.simproc)]))
+  #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"}))
 *}
 
+simproc_setup fast_arith_hypreal ("(m::hypreal) < n" | "(m::hypreal) <= n" | "(m::hypreal) = n") =
+  {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
+
 
 subsection {* Exponentials on the Hyperreals *}
 

--- a/src/HOL/Nat.thy	Wed Jun 29 17:35:46 2011 +0200
+++ b/src/HOL/Nat.thy	Wed Jun 29 18:12:34 2011 +0200
@@ -1433,6 +1433,15 @@
 setup {* Lin_Arith.global_setup *}
 declaration {* K Lin_Arith.setup *}
 
+simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) <= n" | "(m::nat) = n") =
+  {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
+(* Because of this simproc, the arithmetic solver is really only
+useful to detect inconsistencies among the premises for subgoals which are
+*not* themselves (in)equalities, because the latter activate
+fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
+solver all the time rather than add the additional check. *)
+
+
 lemmas [arith_split] = nat_diff_split split_min split_max
 
 context order

--- a/src/HOL/Product_Type.thy	Wed Jun 29 17:35:46 2011 +0200
+++ b/src/HOL/Product_Type.thy	Wed Jun 29 18:12:34 2011 +0200
@@ -556,6 +556,7 @@
         if Pair_pat k i (t $ u) then incr_boundvars k arg
         else (subst arg k i t $ subst arg k i u)
     | subst arg k i t = t;
+in
   fun beta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t) $ arg) =
         (case split_pat beta_term_pat 1 t of
           SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f))
@@ -566,13 +567,10 @@
           SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
         | NONE => NONE)
     | eta_proc _ _ = NONE;
-in
-  val split_beta_proc = Simplifier.simproc_global @{theory} "split_beta" ["split f z"] (K beta_proc);
-  val split_eta_proc = Simplifier.simproc_global @{theory} "split_eta" ["split f"] (K eta_proc);
 end;
-
-Addsimprocs [split_beta_proc, split_eta_proc];
 *}
+simproc_setup split_beta ("split f z") = {* fn _ => fn ss => fn ct => beta_proc ss (term_of ct) *}
+simproc_setup split_eta ("split f") = {* fn _ => fn ss => fn ct => eta_proc ss (term_of ct) *}
 
 lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)"
   by (subst surjective_pairing, rule split_conv)

--- a/src/HOL/Tools/int_arith.ML	Wed Jun 29 17:35:46 2011 +0200
+++ b/src/HOL/Tools/int_arith.ML	Wed Jun 29 18:12:34 2011 +0200
@@ -6,7 +6,6 @@
 signature INT_ARITH =
 sig
   val setup: Context.generic -> Context.generic
-  val global_setup: theory -> theory
 end
 
 structure Int_Arith : INT_ARITH =
@@ -78,16 +77,6 @@
   make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
   proc = sproc, identifier = []}
 
-val fast_int_arith_simproc =
-  Simplifier.simproc_global @{theory} "fast_int_arith"
-     ["(m::'a::{linordered_idom,number_ring}) < n",
-      "(m::'a::{linordered_idom,number_ring}) <= n",
-      "(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
-
-val global_setup =
-  Simplifier.map_simpset_global (fn ss => ss addsimprocs [fast_int_arith_simproc]);
-
-
 fun number_of thy T n =
   if not (Sign.of_sort thy (T, @{sort number}))
   then raise CTERM ("number_of", [])

--- a/src/HOL/Tools/lin_arith.ML	Wed Jun 29 17:35:46 2011 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Wed Jun 29 18:12:34 2011 +0200
@@ -894,15 +894,8 @@
 
 val setup =
   init_arith_data #>
-  Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc_global @{theory} "fast_nat_arith"
-    ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K simproc)]
-    (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
-    useful to detect inconsistencies among the premises for subgoals which are
-    *not* themselves (in)equalities, because the latter activate
-    fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
-    solver all the time rather than add the additional check. *)
-    addSolver (mk_solver' "lin_arith"
-      (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)))
+  Simplifier.map_ss (fn ss => ss
+    addSolver (mk_solver' "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)));
 
 val global_setup =
   Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))