--- a/src/HOL/Statespace/state_fun.ML Fri Dec 17 14:09:37 2010 +0100
+++ b/src/HOL/Statespace/state_fun.ML Fri Dec 17 16:25:21 2010 +0100
@@ -141,8 +141,7 @@
(Const ("StateFun.lookup",lT)$destr$n$(fst (mk_upds s)));
val ctxt = Simplifier.the_context ss;
val basic_ss = #1 (StateFunData.get (Context.Proof ctxt));
- val ss' = Simplifier.context
- (Config.put MetaSimplifier.simp_depth_limit 100 ctxt) basic_ss;
+ val ss' = Simplifier.context (Config.put simp_depth_limit 100 ctxt) basic_ss;
val thm = Simplifier.rewrite ss' ct;
in if (op aconv) (Logic.dest_equals (prop_of thm))
then NONE
@@ -232,8 +231,7 @@
end
| mk_updterm _ t = init_seed t;
- val ctxt = Simplifier.the_context ss |>
- Config.put MetaSimplifier.simp_depth_limit 100;
+ val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100;
val ss1 = Simplifier.context ctxt ss';
val ss2 = Simplifier.context ctxt
(#1 (StateFunData.get (Context.Proof ctxt)));
@@ -266,8 +264,7 @@
Simplifier.simproc_global @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"]
(fn thy => fn ss => fn t =>
let
- val ctxt = Simplifier.the_context ss |>
- Config.put MetaSimplifier.simp_depth_limit 100
+ val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100;
val ex_lookup_ss = #2 (StateFunData.get (Context.Proof ctxt));
val ss' = (Simplifier.context ctxt ex_lookup_ss);
fun prove prop =
--- a/src/Pure/ProofGeneral/preferences.ML Fri Dec 17 14:09:37 2010 +0100
+++ b/src/Pure/ProofGeneral/preferences.ML Fri Dec 17 16:25:21 2010 +0100
@@ -147,10 +147,10 @@
"Show leading question mark of variable name"];
val tracing_preferences =
- [bool_pref simp_trace_default
+ [bool_pref MetaSimplifier.simp_trace_default
"trace-simplifier"
"Trace simplification rules.",
- nat_pref simp_trace_depth_limit_default
+ nat_pref MetaSimplifier.simp_trace_depth_limit_default
"trace-simplifier-depth"
"Trace simplifier depth limit.",
bool_pref trace_rules
--- a/src/Pure/meta_simplifier.ML Fri Dec 17 14:09:37 2010 +0100
+++ b/src/Pure/meta_simplifier.ML Fri Dec 17 16:25:21 2010 +0100
@@ -11,14 +11,10 @@
signature BASIC_META_SIMPLIFIER =
sig
+ val simp_depth_limit: int Config.T
+ val simp_trace_depth_limit: int Config.T
val simp_debug: bool Config.T
- val simp_debug_raw: Config.raw
val simp_trace: bool Config.T
- val simp_trace_raw: Config.raw
- val simp_trace_default: bool Unsynchronized.ref
- val simp_trace_depth_limit: int Config.T
- val simp_trace_depth_limit_raw: Config.raw
- val simp_trace_depth_limit_default: int Unsynchronized.ref
type rrule
val eq_rrule: rrule * rrule -> bool
type simpset
@@ -106,12 +102,16 @@
val del_simp: thm -> simpset -> simpset
val solver: simpset -> solver -> int -> tactic
val simp_depth_limit_raw: Config.raw
- val simp_depth_limit: int Config.T
val clear_ss: simpset -> simpset
val simproc_global_i: theory -> string -> term list
-> (theory -> simpset -> term -> thm option) -> simproc
val simproc_global: theory -> string -> string list
-> (theory -> simpset -> term -> thm option) -> simproc
+ val simp_trace_depth_limit_raw: Config.raw
+ val simp_trace_depth_limit_default: int Unsynchronized.ref
+ val simp_trace_default: bool Unsynchronized.ref
+ val simp_trace_raw: Config.raw
+ val simp_debug_raw: Config.raw
val add_prems: thm list -> simpset -> simpset
val inherit_context: simpset -> simpset -> simpset
val the_context: simpset -> Proof.context