renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
authorwenzelm
Wed Aug 25 18:36:22 2010 +0200 (2010-08-25)
changeset 387156513ea67d95d
parent 38714 31da698fc4e5
child 38716 3c3b4ad683d5
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
src/FOL/simpdata.ML
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Divides.thy
src/HOL/HOL.thy
src/HOL/Import/shuffler.ML
src/HOL/List.thy
src/HOL/NSA/HyperDef.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Orderings.thy
src/HOL/Product_Type.thy
src/HOL/Set.thy
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/SMT/smt_real.ML
src/HOL/Tools/SMT/z3_proof_tools.ML
src/HOL/Tools/abel_cancel.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/nat_arith.ML
src/HOL/Tools/record.ML
src/HOL/Tools/simpdata.ML
src/HOLCF/Tools/cont_proc.ML
src/Pure/meta_simplifier.ML
src/Pure/simplifier.ML
src/Tools/induct.ML
src/ZF/Datatype_ZF.thy
src/ZF/OrdQuant.thy
src/ZF/arith_data.ML
src/ZF/int_arith.ML
src/ZF/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Wed Aug 25 18:19:04 2010 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Wed Aug 25 18:36:22 2010 +0200
     1.3 @@ -81,11 +81,11 @@
     1.4  end);
     1.5  
     1.6  val defEX_regroup =
     1.7 -  Simplifier.simproc @{theory}
     1.8 +  Simplifier.simproc_global @{theory}
     1.9      "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
    1.10  
    1.11  val defALL_regroup =
    1.12 -  Simplifier.simproc @{theory}
    1.13 +  Simplifier.simproc_global @{theory}
    1.14      "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
    1.15  
    1.16  
     2.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Wed Aug 25 18:19:04 2010 +0200
     2.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Wed Aug 25 18:36:22 2010 +0200
     2.3 @@ -285,7 +285,7 @@
     2.4          else SOME rew
     2.5      end;
     2.6    in
     2.7 -    val ring_simproc = Simplifier.simproc @{theory} "ring" lhss (K proc);
     2.8 +    val ring_simproc = Simplifier.simproc_global @{theory} "ring" lhss (K proc);
     2.9    end;
    2.10  *}
    2.11  
     3.1 --- a/src/HOL/Divides.thy	Wed Aug 25 18:19:04 2010 +0200
     3.2 +++ b/src/HOL/Divides.thy	Wed Aug 25 18:36:22 2010 +0200
     3.3 @@ -700,7 +700,7 @@
     3.4  
     3.5  in
     3.6  
     3.7 -val cancel_div_mod_nat_proc = Simplifier.simproc @{theory}
     3.8 +val cancel_div_mod_nat_proc = Simplifier.simproc_global @{theory}
     3.9    "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
    3.10  
    3.11  val _ = Addsimprocs [cancel_div_mod_nat_proc];
    3.12 @@ -1459,7 +1459,7 @@
    3.13  
    3.14  in
    3.15  
    3.16 -val cancel_div_mod_int_proc = Simplifier.simproc @{theory}
    3.17 +val cancel_div_mod_int_proc = Simplifier.simproc_global @{theory}
    3.18    "cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
    3.19  
    3.20  val _ = Addsimprocs [cancel_div_mod_int_proc];
     4.1 --- a/src/HOL/HOL.thy	Wed Aug 25 18:19:04 2010 +0200
     4.2 +++ b/src/HOL/HOL.thy	Wed Aug 25 18:36:22 2010 +0200
     4.3 @@ -1491,13 +1491,13 @@
     4.4        map (Simplifier.rewrite_rule (map Thm.symmetric
     4.5          @{thms induct_rulify_fallback})))
     4.6      addsimprocs
     4.7 -      [Simplifier.simproc @{theory} "swap_induct_false"
     4.8 +      [Simplifier.simproc_global @{theory} "swap_induct_false"
     4.9           ["induct_false ==> PROP P ==> PROP Q"]
    4.10           (fn _ => fn _ =>
    4.11              (fn _ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) =>
    4.12                    if P <> Q then SOME Drule.swap_prems_eq else NONE
    4.13                | _ => NONE)),
    4.14 -       Simplifier.simproc @{theory} "induct_equal_conj_curry"
    4.15 +       Simplifier.simproc_global @{theory} "induct_equal_conj_curry"
    4.16           ["induct_conj P Q ==> PROP R"]
    4.17           (fn _ => fn _ =>
    4.18              (fn _ $ (_ $ P) $ _ =>
    4.19 @@ -1797,7 +1797,7 @@
    4.20  
    4.21  setup {*
    4.22    Code_Preproc.map_pre (fn simpset =>
    4.23 -    simpset addsimprocs [Simplifier.simproc_i @{theory} "eq" [@{term "op ="}]
    4.24 +    simpset addsimprocs [Simplifier.simproc_global_i @{theory} "eq" [@{term "op ="}]
    4.25        (fn thy => fn _ => fn Const (_, T) => case strip_type T
    4.26          of (Type _ :: _, _) => SOME @{thm equals_eq}
    4.27           | _ => NONE)])
     5.1 --- a/src/HOL/Import/shuffler.ML	Wed Aug 25 18:19:04 2010 +0200
     5.2 +++ b/src/HOL/Import/shuffler.ML	Wed Aug 25 18:36:22 2010 +0200
     5.3 @@ -421,29 +421,29 @@
     5.4  val S  = mk_free "S" xT
     5.5  val S'  = mk_free "S'" xT
     5.6  in
     5.7 -fun beta_simproc thy = Simplifier.simproc_i
     5.8 +fun beta_simproc thy = Simplifier.simproc_global_i
     5.9                        thy
    5.10                        "Beta-contraction"
    5.11                        [Abs("x",xT,Q) $ S]
    5.12                        beta_fun
    5.13  
    5.14 -fun equals_simproc thy = Simplifier.simproc_i
    5.15 +fun equals_simproc thy = Simplifier.simproc_global_i
    5.16                        thy
    5.17                        "Ordered rewriting of meta equalities"
    5.18                        [Const("op ==",xT) $ S $ S']
    5.19                        equals_fun
    5.20  
    5.21 -fun quant_simproc thy = Simplifier.simproc_i
    5.22 +fun quant_simproc thy = Simplifier.simproc_global_i
    5.23                             thy
    5.24                             "Ordered rewriting of nested quantifiers"
    5.25                             [Logic.all x (Logic.all y (P $ x $ y))]
    5.26                             quant_rewrite
    5.27 -fun eta_expand_simproc thy = Simplifier.simproc_i
    5.28 +fun eta_expand_simproc thy = Simplifier.simproc_global_i
    5.29                           thy
    5.30                           "Smart eta-expansion by equivalences"
    5.31                           [Logic.mk_equals(Q,R)]
    5.32                           eta_expand
    5.33 -fun eta_contract_simproc thy = Simplifier.simproc_i
    5.34 +fun eta_contract_simproc thy = Simplifier.simproc_global_i
    5.35                           thy
    5.36                           "Smart handling of eta-contractions"
    5.37                           [Logic.all x (Logic.mk_equals (Q $ x, R $ x))]
     6.1 --- a/src/HOL/List.thy	Wed Aug 25 18:19:04 2010 +0200
     6.2 +++ b/src/HOL/List.thy	Wed Aug 25 18:36:22 2010 +0200
     6.3 @@ -732,7 +732,7 @@
     6.4  in
     6.5  
     6.6  val list_eq_simproc =
     6.7 -  Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
     6.8 +  Simplifier.simproc_global @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
     6.9  
    6.10  end;
    6.11  
     7.1 --- a/src/HOL/NSA/HyperDef.thy	Wed Aug 25 18:19:04 2010 +0200
     7.2 +++ b/src/HOL/NSA/HyperDef.thy	Wed Aug 25 18:36:22 2010 +0200
     7.3 @@ -349,7 +349,7 @@
     7.4        @{thm star_of_number_of}, @{thm star_of_add}, @{thm star_of_minus},
     7.5        @{thm star_of_diff}, @{thm star_of_mult}]
     7.6    #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"})
     7.7 -  #> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc @{theory}
     7.8 +  #> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc_global @{theory}
     7.9        "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
    7.10        (K Lin_Arith.simproc)]))
    7.11  *}
     8.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Aug 25 18:19:04 2010 +0200
     8.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Aug 25 18:36:22 2010 +0200
     8.3 @@ -146,7 +146,7 @@
     8.4    | perm_simproc' thy ss _ = NONE;
     8.5  
     8.6  val perm_simproc =
     8.7 -  Simplifier.simproc @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
     8.8 +  Simplifier.simproc_global @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
     8.9  
    8.10  val meta_spec = thm "meta_spec";
    8.11  
     9.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Aug 25 18:19:04 2010 +0200
     9.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Aug 25 18:36:22 2010 +0200
     9.3 @@ -40,7 +40,7 @@
     9.4  fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
     9.5    [(perm_boolI_pi, pi)] perm_boolI;
     9.6  
     9.7 -fun mk_perm_bool_simproc names = Simplifier.simproc_i
     9.8 +fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
     9.9    (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss =>
    9.10      fn Const ("Nominal.perm", _) $ _ $ t =>
    9.11           if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
    10.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Aug 25 18:19:04 2010 +0200
    10.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Aug 25 18:36:22 2010 +0200
    10.3 @@ -8,7 +8,8 @@
    10.4  
    10.5  signature NOMINAL_INDUCTIVE2 =
    10.6  sig
    10.7 -  val prove_strong_ind: string -> string option -> (string * string list) list -> local_theory -> Proof.state
    10.8 +  val prove_strong_ind: string -> string option -> (string * string list) list ->
    10.9 +    local_theory -> Proof.state
   10.10  end
   10.11  
   10.12  structure NominalInductive2 : NOMINAL_INDUCTIVE2 =
   10.13 @@ -43,7 +44,7 @@
   10.14  fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
   10.15    [(perm_boolI_pi, pi)] perm_boolI;
   10.16  
   10.17 -fun mk_perm_bool_simproc names = Simplifier.simproc_i
   10.18 +fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
   10.19    (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss =>
   10.20      fn Const ("Nominal.perm", _) $ _ $ t =>
   10.21           if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
    11.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Wed Aug 25 18:19:04 2010 +0200
    11.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Aug 25 18:36:22 2010 +0200
    11.3 @@ -114,7 +114,7 @@
    11.4        | _ => NONE
    11.5    end
    11.6  
    11.7 -val perm_simproc_app = Simplifier.simproc @{theory} "perm_simproc_app"
    11.8 +val perm_simproc_app = Simplifier.simproc_global @{theory} "perm_simproc_app"
    11.9    ["Nominal.perm pi x"] perm_simproc_app';
   11.10  
   11.11  (* a simproc that deals with permutation instances in front of functions  *)
   11.12 @@ -134,7 +134,7 @@
   11.13        | _ => NONE
   11.14     end
   11.15  
   11.16 -val perm_simproc_fun = Simplifier.simproc @{theory} "perm_simproc_fun"
   11.17 +val perm_simproc_fun = Simplifier.simproc_global @{theory} "perm_simproc_fun"
   11.18    ["Nominal.perm pi x"] perm_simproc_fun';
   11.19  
   11.20  (* function for simplyfying permutations          *)
   11.21 @@ -214,7 +214,7 @@
   11.22      end
   11.23    | _ => NONE);
   11.24  
   11.25 -val perm_compose_simproc = Simplifier.simproc @{theory} "perm_compose"
   11.26 +val perm_compose_simproc = Simplifier.simproc_global @{theory} "perm_compose"
   11.27    ["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc';
   11.28  
   11.29  fun perm_compose_tac ss i = 
    12.1 --- a/src/HOL/Orderings.thy	Wed Aug 25 18:19:04 2010 +0200
    12.2 +++ b/src/HOL/Orderings.thy	Wed Aug 25 18:36:22 2010 +0200
    12.3 @@ -566,7 +566,7 @@
    12.4  fun add_simprocs procs thy =
    12.5    Simplifier.map_simpset (fn ss => ss
    12.6      addsimprocs (map (fn (name, raw_ts, proc) =>
    12.7 -      Simplifier.simproc thy name raw_ts proc) procs)) thy;
    12.8 +      Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
    12.9  fun add_solver name tac =
   12.10    Simplifier.map_simpset (fn ss => ss addSolver
   12.11      mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));
    13.1 --- a/src/HOL/Product_Type.thy	Wed Aug 25 18:19:04 2010 +0200
    13.2 +++ b/src/HOL/Product_Type.thy	Wed Aug 25 18:36:22 2010 +0200
    13.3 @@ -58,7 +58,7 @@
    13.4  ML {*
    13.5    val unit_eq_proc =
    13.6      let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in
    13.7 -      Simplifier.simproc @{theory} "unit_eq" ["x::unit"]
    13.8 +      Simplifier.simproc_global @{theory} "unit_eq" ["x::unit"]
    13.9        (fn _ => fn _ => fn t => if HOLogic.is_unit t then NONE else SOME unit_meta_eq)
   13.10      end;
   13.11  
   13.12 @@ -550,8 +550,8 @@
   13.13          | NONE => NONE)
   13.14      | eta_proc _ _ = NONE;
   13.15  in
   13.16 -  val split_beta_proc = Simplifier.simproc @{theory} "split_beta" ["split f z"] (K beta_proc);
   13.17 -  val split_eta_proc = Simplifier.simproc @{theory} "split_eta" ["split f"] (K eta_proc);
   13.18 +  val split_beta_proc = Simplifier.simproc_global @{theory} "split_beta" ["split f z"] (K beta_proc);
   13.19 +  val split_eta_proc = Simplifier.simproc_global @{theory} "split_eta" ["split f"] (K eta_proc);
   13.20  end;
   13.21  
   13.22  Addsimprocs [split_beta_proc, split_eta_proc];
    14.1 --- a/src/HOL/Set.thy	Wed Aug 25 18:19:04 2010 +0200
    14.2 +++ b/src/HOL/Set.thy	Wed Aug 25 18:36:22 2010 +0200
    14.3 @@ -78,7 +78,7 @@
    14.4    val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
    14.5      ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
    14.6                      DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
    14.7 -  val defColl_regroup = Simplifier.simproc @{theory}
    14.8 +  val defColl_regroup = Simplifier.simproc_global @{theory}
    14.9      "defined Collect" ["{x. P x & Q x}"]
   14.10      (Quantifier1.rearrange_Coll Coll_perm_tac)
   14.11  in
   14.12 @@ -323,9 +323,9 @@
   14.13    val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
   14.14    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
   14.15    val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
   14.16 -  val defBEX_regroup = Simplifier.simproc @{theory}
   14.17 +  val defBEX_regroup = Simplifier.simproc_global @{theory}
   14.18      "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
   14.19 -  val defBALL_regroup = Simplifier.simproc @{theory}
   14.20 +  val defBALL_regroup = Simplifier.simproc_global @{theory}
   14.21      "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
   14.22  in
   14.23    Simplifier.map_simpset (fn ss => ss addsimprocs [defBALL_regroup, defBEX_regroup])
    15.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Wed Aug 25 18:19:04 2010 +0200
    15.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Wed Aug 25 18:36:22 2010 +0200
    15.3 @@ -355,7 +355,7 @@
    15.4                  | NONE => fn i => no_tac)
    15.5  
    15.6  fun distinct_simproc names =
    15.7 -  Simplifier.simproc @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
    15.8 +  Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
    15.9      (fn thy => fn ss => fn (Const (@{const_name "op ="},_)$x$y) =>
   15.10          case try Simplifier.the_context ss of
   15.11          SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq]) 
    16.1 --- a/src/HOL/Statespace/state_fun.ML	Wed Aug 25 18:19:04 2010 +0200
    16.2 +++ b/src/HOL/Statespace/state_fun.ML	Wed Aug 25 18:36:22 2010 +0200
    16.3 @@ -51,7 +51,7 @@
    16.4  in
    16.5  
    16.6  val lazy_conj_simproc =
    16.7 -  Simplifier.simproc @{theory HOL} "lazy_conj_simp" ["P & Q"]
    16.8 +  Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"]
    16.9      (fn thy => fn ss => fn t =>
   16.10        (case t of (Const (@{const_name "op &"},_)$P$Q) => 
   16.11           let
   16.12 @@ -108,7 +108,7 @@
   16.13    Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false));
   16.14  
   16.15  val lookup_simproc =
   16.16 -  Simplifier.simproc @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"]
   16.17 +  Simplifier.simproc_global @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"]
   16.18      (fn thy => fn ss => fn t =>
   16.19        (case t of (Const ("StateFun.lookup",lT)$destr$n$
   16.20                     (s as Const ("StateFun.update",uT)$_$_$_$_$_)) =>
   16.21 @@ -162,7 +162,7 @@
   16.22    addcongs @{thms block_conj_cong});
   16.23  in
   16.24  val update_simproc =
   16.25 -  Simplifier.simproc @{theory} "update_simp" ["update d c n v s"]
   16.26 +  Simplifier.simproc_global @{theory} "update_simp" ["update d c n v s"]
   16.27      (fn thy => fn ss => fn t =>
   16.28        (case t of ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) =>
   16.29           let 
   16.30 @@ -263,7 +263,7 @@
   16.31       end;
   16.32  in
   16.33  val ex_lookup_eq_simproc =
   16.34 -  Simplifier.simproc @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"]
   16.35 +  Simplifier.simproc_global @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"]
   16.36      (fn thy => fn ss => fn t =>
   16.37         let
   16.38           val ctxt = Simplifier.the_context ss |>
    17.1 --- a/src/HOL/Statespace/state_space.ML	Wed Aug 25 18:19:04 2010 +0200
    17.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Aug 25 18:36:22 2010 +0200
    17.3 @@ -235,7 +235,7 @@
    17.4                  | NONE => fn i => no_tac)
    17.5  
    17.6  val distinct_simproc =
    17.7 -  Simplifier.simproc @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
    17.8 +  Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
    17.9      (fn thy => fn ss => (fn (Const (@{const_name "op ="},_)$(x as Free _)$(y as Free _)) =>
   17.10          (case try Simplifier.the_context ss of
   17.11            SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
    18.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Aug 25 18:19:04 2010 +0200
    18.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Aug 25 18:36:22 2010 +0200
    18.3 @@ -163,7 +163,7 @@
    18.4    val thy = ProofContext.theory_of ctxt
    18.5    val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
    18.6    val bex_pat  = @{term "Bex (Respects (R1 ===> R2)) P"}
    18.7 -  val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
    18.8 +  val simproc = Simplifier.simproc_global_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
    18.9    val simpset = (mk_minimal_ss ctxt)
   18.10                         addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
   18.11                         addsimprocs [simproc]
    19.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Wed Aug 25 18:19:04 2010 +0200
    19.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Wed Aug 25 18:36:22 2010 +0200
    19.3 @@ -127,7 +127,7 @@
    19.4    "x + y = y + x"
    19.5    by auto}
    19.6  
    19.7 -val real_linarith_proc = Simplifier.simproc @{theory} "fast_real_arith" [
    19.8 +val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [
    19.9    "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
   19.10  
   19.11  
    20.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Aug 25 18:19:04 2010 +0200
    20.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Aug 25 18:36:22 2010 +0200
    20.3 @@ -323,11 +323,11 @@
    20.4      addsimps @{thms array_rules}
    20.5      addsimps @{thms z3div_def} addsimps @{thms z3mod_def}
    20.6      addsimprocs [
    20.7 -      Simplifier.simproc @{theory} "fast_int_arith" [
    20.8 +      Simplifier.simproc_global @{theory} "fast_int_arith" [
    20.9          "(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc),
   20.10 -      Simplifier.simproc @{theory} "antisym_le" ["(x::'a::order) <= y"]
   20.11 +      Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"]
   20.12          (K prove_antisym_le),
   20.13 -      Simplifier.simproc @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
   20.14 +      Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
   20.15          (K prove_antisym_less)]
   20.16  
   20.17    structure Simpset = Generic_Data
    21.1 --- a/src/HOL/Tools/abel_cancel.ML	Wed Aug 25 18:19:04 2010 +0200
    21.2 +++ b/src/HOL/Tools/abel_cancel.ML	Wed Aug 25 18:36:22 2010 +0200
    21.3 @@ -87,7 +87,7 @@
    21.4          NONE
    21.5    | solve _ = NONE;
    21.6    
    21.7 -val simproc = Simplifier.simproc @{theory}
    21.8 +val simproc = Simplifier.simproc_global @{theory}
    21.9    "add_ac_proc" ["x + y::'a::ab_semigroup_add"] ((K o K) solve);
   21.10  
   21.11  val cancel_ss = HOL_basic_ss settermless less_agrp
    22.1 --- a/src/HOL/Tools/arith_data.ML	Wed Aug 25 18:19:04 2010 +0200
    22.2 +++ b/src/HOL/Tools/arith_data.ML	Wed Aug 25 18:36:22 2010 +0200
    22.3 @@ -127,6 +127,6 @@
    22.4    | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
    22.5  
    22.6  fun prep_simproc thy (name, pats, proc) =
    22.7 -  Simplifier.simproc thy name pats proc;
    22.8 +  Simplifier.simproc_global thy name pats proc;
    22.9  
   22.10  end;
    23.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Aug 25 18:19:04 2010 +0200
    23.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Aug 25 18:36:22 2010 +0200
    23.3 @@ -32,7 +32,7 @@
    23.4  (**** simplify {(x1, ..., xn). (x1, ..., xn) : S} to S ****)
    23.5  
    23.6  val collect_mem_simproc =
    23.7 -  Simplifier.simproc @{theory Set} "Collect_mem" ["Collect t"] (fn thy => fn ss =>
    23.8 +  Simplifier.simproc_global @{theory Set} "Collect_mem" ["Collect t"] (fn thy => fn ss =>
    23.9      fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t =>
   23.10           let val (u, _, ps) = HOLogic.strip_psplits t
   23.11           in case u of
   23.12 @@ -67,7 +67,7 @@
   23.13  val anyt = Free ("t", TFree ("'t", []));
   23.14  
   23.15  fun strong_ind_simproc tab =
   23.16 -  Simplifier.simproc_i @{theory HOL} "strong_ind" [anyt] (fn thy => fn ss => fn t =>
   23.17 +  Simplifier.simproc_global_i @{theory HOL} "strong_ind" [anyt] (fn thy => fn ss => fn t =>
   23.18      let
   23.19        fun close p t f =
   23.20          let val vs = Term.add_vars t []
   23.21 @@ -320,7 +320,7 @@
   23.22  fun to_pred_simproc rules =
   23.23    let val rules' = map mk_meta_eq rules
   23.24    in
   23.25 -    Simplifier.simproc_i @{theory HOL} "to_pred" [anyt]
   23.26 +    Simplifier.simproc_global_i @{theory HOL} "to_pred" [anyt]
   23.27        (fn thy => K (lookup_rule thy (prop_of #> Logic.dest_equals) rules'))
   23.28    end;
   23.29  
    24.1 --- a/src/HOL/Tools/int_arith.ML	Wed Aug 25 18:19:04 2010 +0200
    24.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Aug 25 18:36:22 2010 +0200
    24.3 @@ -79,7 +79,7 @@
    24.4    proc = sproc, identifier = []}
    24.5  
    24.6  val fast_int_arith_simproc =
    24.7 -  Simplifier.simproc @{theory} "fast_int_arith"
    24.8 +  Simplifier.simproc_global @{theory} "fast_int_arith"
    24.9       ["(m::'a::{linordered_idom,number_ring}) < n",
   24.10        "(m::'a::{linordered_idom,number_ring}) <= n",
   24.11        "(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
    25.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Aug 25 18:19:04 2010 +0200
    25.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Aug 25 18:36:22 2010 +0200
    25.3 @@ -910,7 +910,7 @@
    25.4  
    25.5  val setup =
    25.6    init_arith_data #>
    25.7 -  Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc (@{theory}) "fast_nat_arith"
    25.8 +  Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc_global (@{theory}) "fast_nat_arith"
    25.9      ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K simproc)]
   25.10      (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
   25.11      useful to detect inconsistencies among the premises for subgoals which are
    26.1 --- a/src/HOL/Tools/nat_arith.ML	Wed Aug 25 18:19:04 2010 +0200
    26.2 +++ b/src/HOL/Tools/nat_arith.ML	Wed Aug 25 18:36:22 2010 +0200
    26.3 @@ -91,18 +91,18 @@
    26.4  end);
    26.5  
    26.6  val nat_cancel_sums_add =
    26.7 -  [Simplifier.simproc @{theory} "nateq_cancel_sums"
    26.8 +  [Simplifier.simproc_global @{theory} "nateq_cancel_sums"
    26.9       ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
   26.10       (K EqCancelSums.proc),
   26.11 -   Simplifier.simproc @{theory} "natless_cancel_sums"
   26.12 +   Simplifier.simproc_global @{theory} "natless_cancel_sums"
   26.13       ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
   26.14       (K LessCancelSums.proc),
   26.15 -   Simplifier.simproc @{theory} "natle_cancel_sums"
   26.16 +   Simplifier.simproc_global @{theory} "natle_cancel_sums"
   26.17       ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
   26.18       (K LeCancelSums.proc)];
   26.19  
   26.20  val nat_cancel_sums = nat_cancel_sums_add @
   26.21 -  [Simplifier.simproc @{theory} "natdiff_cancel_sums"
   26.22 +  [Simplifier.simproc_global @{theory} "natdiff_cancel_sums"
   26.23      ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
   26.24      (K DiffCancelSums.proc)];
   26.25  
    27.1 --- a/src/HOL/Tools/record.ML	Wed Aug 25 18:19:04 2010 +0200
    27.2 +++ b/src/HOL/Tools/record.ML	Wed Aug 25 18:36:22 2010 +0200
    27.3 @@ -1172,7 +1172,7 @@
    27.4      subrecord.
    27.5  *)
    27.6  val simproc =
    27.7 -  Simplifier.simproc @{theory HOL} "record_simp" ["x"]
    27.8 +  Simplifier.simproc_global @{theory HOL} "record_simp" ["x"]
    27.9      (fn thy => fn _ => fn t =>
   27.10        (case t of
   27.11          (sel as Const (s, Type (_, [_, rangeS]))) $
   27.12 @@ -1246,7 +1246,7 @@
   27.13    we omit considering further updates if doing so would introduce
   27.14    both a more update and an update to a field within it.*)
   27.15  val upd_simproc =
   27.16 -  Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
   27.17 +  Simplifier.simproc_global @{theory HOL} "record_upd_simp" ["x"]
   27.18      (fn thy => fn _ => fn t =>
   27.19        let
   27.20          (*We can use more-updators with other updators as long
   27.21 @@ -1366,7 +1366,7 @@
   27.22   Complexity: #components * #updates     #updates
   27.23  *)
   27.24  val eq_simproc =
   27.25 -  Simplifier.simproc @{theory HOL} "record_eq_simp" ["r = s"]
   27.26 +  Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
   27.27      (fn thy => fn _ => fn t =>
   27.28        (case t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ =>
   27.29          (case rec_id ~1 T of
   27.30 @@ -1386,7 +1386,7 @@
   27.31      P t = ~1: completely split
   27.32      P t > 0: split up to given bound of record extensions.*)
   27.33  fun split_simproc P =
   27.34 -  Simplifier.simproc @{theory HOL} "record_split_simp" ["x"]
   27.35 +  Simplifier.simproc_global @{theory HOL} "record_split_simp" ["x"]
   27.36      (fn thy => fn _ => fn t =>
   27.37        (case t of
   27.38          Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
   27.39 @@ -1414,7 +1414,7 @@
   27.40        | _ => NONE));
   27.41  
   27.42  val ex_sel_eq_simproc =
   27.43 -  Simplifier.simproc @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
   27.44 +  Simplifier.simproc_global @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
   27.45      (fn thy => fn ss => fn t =>
   27.46        let
   27.47          fun prove prop =
    28.1 --- a/src/HOL/Tools/simpdata.ML	Wed Aug 25 18:19:04 2010 +0200
    28.2 +++ b/src/HOL/Tools/simpdata.ML	Wed Aug 25 18:36:22 2010 +0200
    28.3 @@ -182,11 +182,11 @@
    28.4    in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
    28.5  
    28.6  val defALL_regroup =
    28.7 -  Simplifier.simproc @{theory}
    28.8 +  Simplifier.simproc_global @{theory}
    28.9      "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
   28.10  
   28.11  val defEX_regroup =
   28.12 -  Simplifier.simproc @{theory}
   28.13 +  Simplifier.simproc_global @{theory}
   28.14      "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
   28.15  
   28.16  
    29.1 --- a/src/HOLCF/Tools/cont_proc.ML	Wed Aug 25 18:19:04 2010 +0200
    29.2 +++ b/src/HOLCF/Tools/cont_proc.ML	Wed Aug 25 18:36:22 2010 +0200
    29.3 @@ -128,7 +128,7 @@
    29.4      in Option.map fst (Seq.pull (cont_tac 1 tr)) end
    29.5  in
    29.6    fun cont_proc thy =
    29.7 -    Simplifier.simproc thy "cont_proc" ["cont f"] solve_cont;
    29.8 +    Simplifier.simproc_global thy "cont_proc" ["cont f"] solve_cont;
    29.9  end;
   29.10  
   29.11  fun setup thy = Simplifier.map_simpset (fn ss => ss addsimprocs [cont_proc thy]) thy;
    30.1 --- a/src/Pure/meta_simplifier.ML	Wed Aug 25 18:19:04 2010 +0200
    30.2 +++ b/src/Pure/meta_simplifier.ML	Wed Aug 25 18:36:22 2010 +0200
    30.3 @@ -107,9 +107,9 @@
    30.4    val simp_depth_limit_value: Config.value Config.T
    30.5    val simp_depth_limit: int Config.T
    30.6    val clear_ss: simpset -> simpset
    30.7 -  val simproc_i: theory -> string -> term list
    30.8 +  val simproc_global_i: theory -> string -> term list
    30.9      -> (theory -> simpset -> term -> thm option) -> simproc
   30.10 -  val simproc: theory -> string -> string list
   30.11 +  val simproc_global: theory -> string -> string list
   30.12      -> (theory -> simpset -> term -> thm option) -> simproc
   30.13    val inherit_context: simpset -> simpset -> simpset
   30.14    val the_context: simpset -> Proof.context
   30.15 @@ -631,8 +631,8 @@
   30.16      proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
   30.17  
   30.18  (* FIXME avoid global thy and Logic.varify_global *)
   30.19 -fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
   30.20 -fun simproc thy name = simproc_i thy name o map (Syntax.read_term_global thy);
   30.21 +fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
   30.22 +fun simproc_global thy name = simproc_global_i thy name o map (Syntax.read_term_global thy);
   30.23  
   30.24  
   30.25  local
    31.1 --- a/src/Pure/simplifier.ML	Wed Aug 25 18:19:04 2010 +0200
    31.2 +++ b/src/Pure/simplifier.ML	Wed Aug 25 18:36:22 2010 +0200
    31.3 @@ -38,9 +38,9 @@
    31.4    val context: Proof.context -> simpset -> simpset
    31.5    val global_context: theory -> simpset -> simpset
    31.6    val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
    31.7 -  val simproc_i: theory -> string -> term list
    31.8 +  val simproc_global_i: theory -> string -> term list
    31.9      -> (theory -> simpset -> term -> thm option) -> simproc
   31.10 -  val simproc: theory -> string -> string list
   31.11 +  val simproc_global: theory -> string -> string list
   31.12      -> (theory -> simpset -> term -> thm option) -> simproc
   31.13    val rewrite: simpset -> conv
   31.14    val asm_rewrite: simpset -> conv
    32.1 --- a/src/Tools/induct.ML	Wed Aug 25 18:19:04 2010 +0200
    32.2 +++ b/src/Tools/induct.ML	Wed Aug 25 18:36:22 2010 +0200
    32.3 @@ -152,7 +152,7 @@
    32.4    | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
    32.5  
    32.6  val rearrange_eqs_simproc =
    32.7 -  Simplifier.simproc
    32.8 +  Simplifier.simproc_global
    32.9      (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"]
   32.10      (fn thy => fn ss => fn t =>
   32.11        mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t));
    33.1 --- a/src/ZF/Datatype_ZF.thy	Wed Aug 25 18:19:04 2010 +0200
    33.2 +++ b/src/ZF/Datatype_ZF.thy	Wed Aug 25 18:36:22 2010 +0200
    33.3 @@ -101,7 +101,7 @@
    33.4     handle Match => NONE;
    33.5  
    33.6  
    33.7 - val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc;
    33.8 + val conv = Simplifier.simproc_global @{theory} "data_free" ["(x::i) = y"] proc;
    33.9  
   33.10  end;
   33.11  
    34.1 --- a/src/ZF/OrdQuant.thy	Wed Aug 25 18:19:04 2010 +0200
    34.2 +++ b/src/ZF/OrdQuant.thy	Wed Aug 25 18:36:22 2010 +0200
    34.3 @@ -381,9 +381,9 @@
    34.4  
    34.5  in
    34.6  
    34.7 -val defREX_regroup = Simplifier.simproc @{theory}
    34.8 +val defREX_regroup = Simplifier.simproc_global @{theory}
    34.9    "defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
   34.10 -val defRALL_regroup = Simplifier.simproc @{theory}
   34.11 +val defRALL_regroup = Simplifier.simproc_global @{theory}
   34.12    "defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
   34.13  
   34.14  end;
    35.1 --- a/src/ZF/arith_data.ML	Wed Aug 25 18:19:04 2010 +0200
    35.2 +++ b/src/ZF/arith_data.ML	Wed Aug 25 18:36:22 2010 +0200
    35.3 @@ -77,7 +77,7 @@
    35.4    end;
    35.5  
    35.6  fun prep_simproc thy (name, pats, proc) =
    35.7 -  Simplifier.simproc thy name pats proc;
    35.8 +  Simplifier.simproc_global thy name pats proc;
    35.9  
   35.10  
   35.11  (*** Use CancelNumerals simproc without binary numerals,
    36.1 --- a/src/ZF/int_arith.ML	Wed Aug 25 18:19:04 2010 +0200
    36.2 +++ b/src/ZF/int_arith.ML	Wed Aug 25 18:36:22 2010 +0200
    36.3 @@ -147,7 +147,7 @@
    36.4      [@{thm zmult_assoc}, @{thm zmult_zminus} RS @{thm sym}, int_minus_mult_eq_1_to_2];
    36.5  
    36.6  fun prep_simproc thy (name, pats, proc) =
    36.7 -  Simplifier.simproc thy name pats proc;
    36.8 +  Simplifier.simproc_global thy name pats proc;
    36.9  
   36.10  structure CancelNumeralsCommon =
   36.11    struct
    37.1 --- a/src/ZF/simpdata.ML	Wed Aug 25 18:19:04 2010 +0200
    37.2 +++ b/src/ZF/simpdata.ML	Wed Aug 25 18:36:22 2010 +0200
    37.3 @@ -59,10 +59,10 @@
    37.4  
    37.5  in
    37.6  
    37.7 -val defBEX_regroup = Simplifier.simproc (Theory.deref @{theory_ref})
    37.8 +val defBEX_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
    37.9    "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
   37.10  
   37.11 -val defBALL_regroup = Simplifier.simproc (Theory.deref @{theory_ref})
   37.12 +val defBALL_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
   37.13    "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
   37.14  
   37.15  end;