# HG changeset patch
# User wenzelm
# Date 1282754182 -7200
# Node ID 6513ea67d95dbfde0ee44555b257076a65f4a58f
# Parent  31da698fc4e578fd573f0191d88e8cbb1b130a12
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;

diff -r 31da698fc4e5 -r 6513ea67d95d src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/FOL/simpdata.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -81,11 +81,11 @@
 end);
 
 val defEX_regroup =
-  Simplifier.simproc @{theory}
+  Simplifier.simproc_global @{theory}
     "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
 
 val defALL_regroup =
-  Simplifier.simproc @{theory}
+  Simplifier.simproc_global @{theory}
     "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
 
 
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Wed Aug 25 18:36:22 2010 +0200
@@ -285,7 +285,7 @@
         else SOME rew
     end;
   in
-    val ring_simproc = Simplifier.simproc @{theory} "ring" lhss (K proc);
+    val ring_simproc = Simplifier.simproc_global @{theory} "ring" lhss (K proc);
   end;
 *}
 
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Divides.thy	Wed Aug 25 18:36:22 2010 +0200
@@ -700,7 +700,7 @@
 
 in
 
-val cancel_div_mod_nat_proc = Simplifier.simproc @{theory}
+val cancel_div_mod_nat_proc = Simplifier.simproc_global @{theory}
   "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
 
 val _ = Addsimprocs [cancel_div_mod_nat_proc];
@@ -1459,7 +1459,7 @@
 
 in
 
-val cancel_div_mod_int_proc = Simplifier.simproc @{theory}
+val cancel_div_mod_int_proc = Simplifier.simproc_global @{theory}
   "cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
 
 val _ = Addsimprocs [cancel_div_mod_int_proc];
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/HOL.thy	Wed Aug 25 18:36:22 2010 +0200
@@ -1491,13 +1491,13 @@
       map (Simplifier.rewrite_rule (map Thm.symmetric
         @{thms induct_rulify_fallback})))
     addsimprocs
-      [Simplifier.simproc @{theory} "swap_induct_false"
+      [Simplifier.simproc_global @{theory} "swap_induct_false"
          ["induct_false ==> PROP P ==> PROP Q"]
          (fn _ => fn _ =>
             (fn _ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) =>
                   if P <> Q then SOME Drule.swap_prems_eq else NONE
               | _ => NONE)),
-       Simplifier.simproc @{theory} "induct_equal_conj_curry"
+       Simplifier.simproc_global @{theory} "induct_equal_conj_curry"
          ["induct_conj P Q ==> PROP R"]
          (fn _ => fn _ =>
             (fn _ $ (_ $ P) $ _ =>
@@ -1797,7 +1797,7 @@
 
 setup {*
   Code_Preproc.map_pre (fn simpset =>
-    simpset addsimprocs [Simplifier.simproc_i @{theory} "eq" [@{term "op ="}]
+    simpset addsimprocs [Simplifier.simproc_global_i @{theory} "eq" [@{term "op ="}]
       (fn thy => fn _ => fn Const (_, T) => case strip_type T
         of (Type _ :: _, _) => SOME @{thm equals_eq}
          | _ => NONE)])
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Import/shuffler.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -421,29 +421,29 @@
 val S  = mk_free "S" xT
 val S'  = mk_free "S'" xT
 in
-fun beta_simproc thy = Simplifier.simproc_i
+fun beta_simproc thy = Simplifier.simproc_global_i
                       thy
                       "Beta-contraction"
                       [Abs("x",xT,Q) $ S]
                       beta_fun
 
-fun equals_simproc thy = Simplifier.simproc_i
+fun equals_simproc thy = Simplifier.simproc_global_i
                       thy
                       "Ordered rewriting of meta equalities"
                       [Const("op ==",xT) $ S $ S']
                       equals_fun
 
-fun quant_simproc thy = Simplifier.simproc_i
+fun quant_simproc thy = Simplifier.simproc_global_i
                            thy
                            "Ordered rewriting of nested quantifiers"
                            [Logic.all x (Logic.all y (P $ x $ y))]
                            quant_rewrite
-fun eta_expand_simproc thy = Simplifier.simproc_i
+fun eta_expand_simproc thy = Simplifier.simproc_global_i
                          thy
                          "Smart eta-expansion by equivalences"
                          [Logic.mk_equals(Q,R)]
                          eta_expand
-fun eta_contract_simproc thy = Simplifier.simproc_i
+fun eta_contract_simproc thy = Simplifier.simproc_global_i
                          thy
                          "Smart handling of eta-contractions"
                          [Logic.all x (Logic.mk_equals (Q $ x, R $ x))]
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/List.thy	Wed Aug 25 18:36:22 2010 +0200
@@ -732,7 +732,7 @@
 in
 
 val list_eq_simproc =
-  Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
+  Simplifier.simproc_global @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
 
 end;
 
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Wed Aug 25 18:36:22 2010 +0200
@@ -349,7 +349,7 @@
       @{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 @{theory}
+  #> 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)]))
 *}
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -146,7 +146,7 @@
   | perm_simproc' thy ss _ = NONE;
 
 val perm_simproc =
-  Simplifier.simproc @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
+  Simplifier.simproc_global @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
 
 val meta_spec = thm "meta_spec";
 
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -40,7 +40,7 @@
 fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
   [(perm_boolI_pi, pi)] perm_boolI;
 
-fun mk_perm_bool_simproc names = Simplifier.simproc_i
+fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
   (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss =>
     fn Const ("Nominal.perm", _) $ _ $ t =>
          if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -8,7 +8,8 @@
 
 signature NOMINAL_INDUCTIVE2 =
 sig
-  val prove_strong_ind: string -> string option -> (string * string list) list -> local_theory -> Proof.state
+  val prove_strong_ind: string -> string option -> (string * string list) list ->
+    local_theory -> Proof.state
 end
 
 structure NominalInductive2 : NOMINAL_INDUCTIVE2 =
@@ -43,7 +44,7 @@
 fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
   [(perm_boolI_pi, pi)] perm_boolI;
 
-fun mk_perm_bool_simproc names = Simplifier.simproc_i
+fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
   (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss =>
     fn Const ("Nominal.perm", _) $ _ $ t =>
          if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -114,7 +114,7 @@
       | _ => NONE
   end
 
-val perm_simproc_app = Simplifier.simproc @{theory} "perm_simproc_app"
+val perm_simproc_app = Simplifier.simproc_global @{theory} "perm_simproc_app"
   ["Nominal.perm pi x"] perm_simproc_app';
 
 (* a simproc that deals with permutation instances in front of functions  *)
@@ -134,7 +134,7 @@
       | _ => NONE
    end
 
-val perm_simproc_fun = Simplifier.simproc @{theory} "perm_simproc_fun"
+val perm_simproc_fun = Simplifier.simproc_global @{theory} "perm_simproc_fun"
   ["Nominal.perm pi x"] perm_simproc_fun';
 
 (* function for simplyfying permutations          *)
@@ -214,7 +214,7 @@
     end
   | _ => NONE);
 
-val perm_compose_simproc = Simplifier.simproc @{theory} "perm_compose"
+val perm_compose_simproc = Simplifier.simproc_global @{theory} "perm_compose"
   ["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc';
 
 fun perm_compose_tac ss i = 
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Orderings.thy	Wed Aug 25 18:36:22 2010 +0200
@@ -566,7 +566,7 @@
 fun add_simprocs procs thy =
   Simplifier.map_simpset (fn ss => ss
     addsimprocs (map (fn (name, raw_ts, proc) =>
-      Simplifier.simproc thy name raw_ts proc) procs)) thy;
+      Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
 fun add_solver name tac =
   Simplifier.map_simpset (fn ss => ss addSolver
     mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Product_Type.thy	Wed Aug 25 18:36:22 2010 +0200
@@ -58,7 +58,7 @@
 ML {*
   val unit_eq_proc =
     let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in
-      Simplifier.simproc @{theory} "unit_eq" ["x::unit"]
+      Simplifier.simproc_global @{theory} "unit_eq" ["x::unit"]
       (fn _ => fn _ => fn t => if HOLogic.is_unit t then NONE else SOME unit_meta_eq)
     end;
 
@@ -550,8 +550,8 @@
         | NONE => NONE)
     | eta_proc _ _ = NONE;
 in
-  val split_beta_proc = Simplifier.simproc @{theory} "split_beta" ["split f z"] (K beta_proc);
-  val split_eta_proc = Simplifier.simproc @{theory} "split_eta" ["split f"] (K eta_proc);
+  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];
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Set.thy	Wed Aug 25 18:36:22 2010 +0200
@@ -78,7 +78,7 @@
   val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
     ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
                     DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
-  val defColl_regroup = Simplifier.simproc @{theory}
+  val defColl_regroup = Simplifier.simproc_global @{theory}
     "defined Collect" ["{x. P x & Q x}"]
     (Quantifier1.rearrange_Coll Coll_perm_tac)
 in
@@ -323,9 +323,9 @@
   val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
   fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
   val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
-  val defBEX_regroup = Simplifier.simproc @{theory}
+  val defBEX_regroup = Simplifier.simproc_global @{theory}
     "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
-  val defBALL_regroup = Simplifier.simproc @{theory}
+  val defBALL_regroup = Simplifier.simproc_global @{theory}
     "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
 in
   Simplifier.map_simpset (fn ss => ss addsimprocs [defBALL_regroup, defBEX_regroup])
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Statespace/distinct_tree_prover.ML
--- a/src/HOL/Statespace/distinct_tree_prover.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -355,7 +355,7 @@
                 | NONE => fn i => no_tac)
 
 fun distinct_simproc names =
-  Simplifier.simproc @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
+  Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
     (fn thy => fn ss => fn (Const (@{const_name "op ="},_)$x$y) =>
         case try Simplifier.the_context ss of
         SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq]) 
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -51,7 +51,7 @@
 in
 
 val lazy_conj_simproc =
-  Simplifier.simproc @{theory HOL} "lazy_conj_simp" ["P & Q"]
+  Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"]
     (fn thy => fn ss => fn t =>
       (case t of (Const (@{const_name "op &"},_)$P$Q) => 
          let
@@ -108,7 +108,7 @@
   Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false));
 
 val lookup_simproc =
-  Simplifier.simproc @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"]
+  Simplifier.simproc_global @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"]
     (fn thy => fn ss => fn t =>
       (case t of (Const ("StateFun.lookup",lT)$destr$n$
                    (s as Const ("StateFun.update",uT)$_$_$_$_$_)) =>
@@ -162,7 +162,7 @@
   addcongs @{thms block_conj_cong});
 in
 val update_simproc =
-  Simplifier.simproc @{theory} "update_simp" ["update d c n v s"]
+  Simplifier.simproc_global @{theory} "update_simp" ["update d c n v s"]
     (fn thy => fn ss => fn t =>
       (case t of ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) =>
          let 
@@ -263,7 +263,7 @@
      end;
 in
 val ex_lookup_eq_simproc =
-  Simplifier.simproc @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"]
+  Simplifier.simproc_global @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"]
     (fn thy => fn ss => fn t =>
        let
          val ctxt = Simplifier.the_context ss |>
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -235,7 +235,7 @@
                 | NONE => fn i => no_tac)
 
 val distinct_simproc =
-  Simplifier.simproc @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
+  Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
     (fn thy => fn ss => (fn (Const (@{const_name "op ="},_)$(x as Free _)$(y as Free _)) =>
         (case try Simplifier.the_context ss of
           SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -163,7 +163,7 @@
   val thy = ProofContext.theory_of ctxt
   val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
   val bex_pat  = @{term "Bex (Respects (R1 ===> R2)) P"}
-  val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
+  val simproc = Simplifier.simproc_global_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
   val simpset = (mk_minimal_ss ctxt)
                        addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
                        addsimprocs [simproc]
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Tools/SMT/smt_real.ML
--- a/src/HOL/Tools/SMT/smt_real.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_real.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -127,7 +127,7 @@
   "x + y = y + x"
   by auto}
 
-val real_linarith_proc = Simplifier.simproc @{theory} "fast_real_arith" [
+val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [
   "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
 
 
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -323,11 +323,11 @@
     addsimps @{thms array_rules}
     addsimps @{thms z3div_def} addsimps @{thms z3mod_def}
     addsimprocs [
-      Simplifier.simproc @{theory} "fast_int_arith" [
+      Simplifier.simproc_global @{theory} "fast_int_arith" [
         "(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc),
-      Simplifier.simproc @{theory} "antisym_le" ["(x::'a::order) <= y"]
+      Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"]
         (K prove_antisym_le),
-      Simplifier.simproc @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
+      Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
         (K prove_antisym_less)]
 
   structure Simpset = Generic_Data
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Tools/abel_cancel.ML
--- a/src/HOL/Tools/abel_cancel.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Tools/abel_cancel.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -87,7 +87,7 @@
         NONE
   | solve _ = NONE;
   
-val simproc = Simplifier.simproc @{theory}
+val simproc = Simplifier.simproc_global @{theory}
   "add_ac_proc" ["x + y::'a::ab_semigroup_add"] ((K o K) solve);
 
 val cancel_ss = HOL_basic_ss settermless less_agrp
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Tools/arith_data.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -127,6 +127,6 @@
   | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
 
 fun prep_simproc thy (name, pats, proc) =
-  Simplifier.simproc thy name pats proc;
+  Simplifier.simproc_global thy name pats proc;
 
 end;
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -32,7 +32,7 @@
 (**** simplify {(x1, ..., xn). (x1, ..., xn) : S} to S ****)
 
 val collect_mem_simproc =
-  Simplifier.simproc @{theory Set} "Collect_mem" ["Collect t"] (fn thy => fn ss =>
+  Simplifier.simproc_global @{theory Set} "Collect_mem" ["Collect t"] (fn thy => fn ss =>
     fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t =>
          let val (u, _, ps) = HOLogic.strip_psplits t
          in case u of
@@ -67,7 +67,7 @@
 val anyt = Free ("t", TFree ("'t", []));
 
 fun strong_ind_simproc tab =
-  Simplifier.simproc_i @{theory HOL} "strong_ind" [anyt] (fn thy => fn ss => fn t =>
+  Simplifier.simproc_global_i @{theory HOL} "strong_ind" [anyt] (fn thy => fn ss => fn t =>
     let
       fun close p t f =
         let val vs = Term.add_vars t []
@@ -320,7 +320,7 @@
 fun to_pred_simproc rules =
   let val rules' = map mk_meta_eq rules
   in
-    Simplifier.simproc_i @{theory HOL} "to_pred" [anyt]
+    Simplifier.simproc_global_i @{theory HOL} "to_pred" [anyt]
       (fn thy => K (lookup_rule thy (prop_of #> Logic.dest_equals) rules'))
   end;
 
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Tools/int_arith.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -79,7 +79,7 @@
   proc = sproc, identifier = []}
 
 val fast_int_arith_simproc =
-  Simplifier.simproc @{theory} "fast_int_arith"
+  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);
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -910,7 +910,7 @@
 
 val setup =
   init_arith_data #>
-  Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc (@{theory}) "fast_nat_arith"
+  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
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Tools/nat_arith.ML
--- a/src/HOL/Tools/nat_arith.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Tools/nat_arith.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -91,18 +91,18 @@
 end);
 
 val nat_cancel_sums_add =
-  [Simplifier.simproc @{theory} "nateq_cancel_sums"
+  [Simplifier.simproc_global @{theory} "nateq_cancel_sums"
      ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
      (K EqCancelSums.proc),
-   Simplifier.simproc @{theory} "natless_cancel_sums"
+   Simplifier.simproc_global @{theory} "natless_cancel_sums"
      ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
      (K LessCancelSums.proc),
-   Simplifier.simproc @{theory} "natle_cancel_sums"
+   Simplifier.simproc_global @{theory} "natle_cancel_sums"
      ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
      (K LeCancelSums.proc)];
 
 val nat_cancel_sums = nat_cancel_sums_add @
-  [Simplifier.simproc @{theory} "natdiff_cancel_sums"
+  [Simplifier.simproc_global @{theory} "natdiff_cancel_sums"
     ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
     (K DiffCancelSums.proc)];
 
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Tools/record.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -1172,7 +1172,7 @@
     subrecord.
 *)
 val simproc =
-  Simplifier.simproc @{theory HOL} "record_simp" ["x"]
+  Simplifier.simproc_global @{theory HOL} "record_simp" ["x"]
     (fn thy => fn _ => fn t =>
       (case t of
         (sel as Const (s, Type (_, [_, rangeS]))) $
@@ -1246,7 +1246,7 @@
   we omit considering further updates if doing so would introduce
   both a more update and an update to a field within it.*)
 val upd_simproc =
-  Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
+  Simplifier.simproc_global @{theory HOL} "record_upd_simp" ["x"]
     (fn thy => fn _ => fn t =>
       let
         (*We can use more-updators with other updators as long
@@ -1366,7 +1366,7 @@
  Complexity: #components * #updates     #updates
 *)
 val eq_simproc =
-  Simplifier.simproc @{theory HOL} "record_eq_simp" ["r = s"]
+  Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
     (fn thy => fn _ => fn t =>
       (case t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ =>
         (case rec_id ~1 T of
@@ -1386,7 +1386,7 @@
     P t = ~1: completely split
     P t > 0: split up to given bound of record extensions.*)
 fun split_simproc P =
-  Simplifier.simproc @{theory HOL} "record_split_simp" ["x"]
+  Simplifier.simproc_global @{theory HOL} "record_split_simp" ["x"]
     (fn thy => fn _ => fn t =>
       (case t of
         Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
@@ -1414,7 +1414,7 @@
       | _ => NONE));
 
 val ex_sel_eq_simproc =
-  Simplifier.simproc @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
+  Simplifier.simproc_global @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
     (fn thy => fn ss => fn t =>
       let
         fun prove prop =
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -182,11 +182,11 @@
   in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
 
 val defALL_regroup =
-  Simplifier.simproc @{theory}
+  Simplifier.simproc_global @{theory}
     "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
 
 val defEX_regroup =
-  Simplifier.simproc @{theory}
+  Simplifier.simproc_global @{theory}
     "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
 
 
diff -r 31da698fc4e5 -r 6513ea67d95d src/HOLCF/Tools/cont_proc.ML
--- a/src/HOLCF/Tools/cont_proc.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOLCF/Tools/cont_proc.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -128,7 +128,7 @@
     in Option.map fst (Seq.pull (cont_tac 1 tr)) end
 in
   fun cont_proc thy =
-    Simplifier.simproc thy "cont_proc" ["cont f"] solve_cont;
+    Simplifier.simproc_global thy "cont_proc" ["cont f"] solve_cont;
 end;
 
 fun setup thy = Simplifier.map_simpset (fn ss => ss addsimprocs [cont_proc thy]) thy;
diff -r 31da698fc4e5 -r 6513ea67d95d src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/Pure/meta_simplifier.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -107,9 +107,9 @@
   val simp_depth_limit_value: Config.value Config.T
   val simp_depth_limit: int Config.T
   val clear_ss: simpset -> simpset
-  val simproc_i: theory -> string -> term list
+  val simproc_global_i: theory -> string -> term list
     -> (theory -> simpset -> term -> thm option) -> simproc
-  val simproc: theory -> string -> string list
+  val simproc_global: theory -> string -> string list
     -> (theory -> simpset -> term -> thm option) -> simproc
   val inherit_context: simpset -> simpset -> simpset
   val the_context: simpset -> Proof.context
@@ -631,8 +631,8 @@
     proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
 
 (* FIXME avoid global thy and Logic.varify_global *)
-fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
-fun simproc thy name = simproc_i thy name o map (Syntax.read_term_global thy);
+fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
+fun simproc_global thy name = simproc_global_i thy name o map (Syntax.read_term_global thy);
 
 
 local
diff -r 31da698fc4e5 -r 6513ea67d95d src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/Pure/simplifier.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -38,9 +38,9 @@
   val context: Proof.context -> simpset -> simpset
   val global_context: theory -> simpset -> simpset
   val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
-  val simproc_i: theory -> string -> term list
+  val simproc_global_i: theory -> string -> term list
     -> (theory -> simpset -> term -> thm option) -> simproc
-  val simproc: theory -> string -> string list
+  val simproc_global: theory -> string -> string list
     -> (theory -> simpset -> term -> thm option) -> simproc
   val rewrite: simpset -> conv
   val asm_rewrite: simpset -> conv
diff -r 31da698fc4e5 -r 6513ea67d95d src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/Tools/induct.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -152,7 +152,7 @@
   | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
 
 val rearrange_eqs_simproc =
-  Simplifier.simproc
+  Simplifier.simproc_global
     (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"]
     (fn thy => fn ss => fn t =>
       mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t));
diff -r 31da698fc4e5 -r 6513ea67d95d src/ZF/Datatype_ZF.thy
--- a/src/ZF/Datatype_ZF.thy	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/ZF/Datatype_ZF.thy	Wed Aug 25 18:36:22 2010 +0200
@@ -101,7 +101,7 @@
    handle Match => NONE;
 
 
- val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc;
+ val conv = Simplifier.simproc_global @{theory} "data_free" ["(x::i) = y"] proc;
 
 end;
 
diff -r 31da698fc4e5 -r 6513ea67d95d src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/ZF/OrdQuant.thy	Wed Aug 25 18:36:22 2010 +0200
@@ -381,9 +381,9 @@
 
 in
 
-val defREX_regroup = Simplifier.simproc @{theory}
+val defREX_regroup = Simplifier.simproc_global @{theory}
   "defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
-val defRALL_regroup = Simplifier.simproc @{theory}
+val defRALL_regroup = Simplifier.simproc_global @{theory}
   "defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
 
 end;
diff -r 31da698fc4e5 -r 6513ea67d95d src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/ZF/arith_data.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -77,7 +77,7 @@
   end;
 
 fun prep_simproc thy (name, pats, proc) =
-  Simplifier.simproc thy name pats proc;
+  Simplifier.simproc_global thy name pats proc;
 
 
 (*** Use CancelNumerals simproc without binary numerals,
diff -r 31da698fc4e5 -r 6513ea67d95d src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/ZF/int_arith.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -147,7 +147,7 @@
     [@{thm zmult_assoc}, @{thm zmult_zminus} RS @{thm sym}, int_minus_mult_eq_1_to_2];
 
 fun prep_simproc thy (name, pats, proc) =
-  Simplifier.simproc thy name pats proc;
+  Simplifier.simproc_global thy name pats proc;
 
 structure CancelNumeralsCommon =
   struct
diff -r 31da698fc4e5 -r 6513ea67d95d src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/ZF/simpdata.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -59,10 +59,10 @@
 
 in
 
-val defBEX_regroup = Simplifier.simproc (Theory.deref @{theory_ref})
+val defBEX_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
   "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
 
-val defBALL_regroup = Simplifier.simproc (Theory.deref @{theory_ref})
+val defBALL_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
   "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
 
 end;