tuned signature;

--- 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