renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
--- 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;
--- 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;
*}
--- 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];
--- 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)])
--- 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))]
--- 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;
--- 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)]))
*}
--- 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";
--- 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))
--- 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))
--- 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 =
--- 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)));
--- 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];
--- 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])
--- 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])
--- 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 |>
--- 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])
--- 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]
--- 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)
--- 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
--- 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
--- 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;
--- 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;
--- 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);
--- 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
--- 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)];
--- 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 =
--- 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;
--- 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;
--- 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
--- 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
--- 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));
--- 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;
--- 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;
--- 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,
--- 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
--- 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;