--- a/src/Pure/meta_simplifier.ML Mon Sep 06 19:23:54 2010 +0200
+++ b/src/Pure/meta_simplifier.ML Mon Sep 06 21:33:19 2010 +0200
@@ -12,9 +12,9 @@
signature BASIC_META_SIMPLIFIER =
sig
val debug_simp: bool Config.T
- val debug_simp_value: Config.value Config.T
+ val debug_simp_raw: Config.raw
val trace_simp: bool Config.T
- val trace_simp_value: Config.value Config.T
+ val trace_simp_raw: Config.raw
val trace_simp_default: bool Unsynchronized.ref
val trace_simp_depth_limit: int Unsynchronized.ref
type rrule
@@ -104,7 +104,7 @@
val add_simp: thm -> simpset -> simpset
val del_simp: thm -> simpset -> simpset
val solver: simpset -> solver -> int -> tactic
- val simp_depth_limit_value: Config.value Config.T
+ 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
@@ -250,8 +250,8 @@
(* simp depth *)
-val simp_depth_limit_value = Config.declare "simp_depth_limit" (K (Config.Int 100));
-val simp_depth_limit = Config.int simp_depth_limit_value;
+val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
+val simp_depth_limit = Config.int simp_depth_limit_raw;
val trace_simp_depth_limit = Unsynchronized.ref 1;
@@ -273,12 +273,12 @@
exception SIMPLIFIER of string * thm;
-val debug_simp_value = Config.declare "debug_simp" (K (Config.Bool false));
-val debug_simp = Config.bool debug_simp_value;
+val debug_simp_raw = Config.declare "debug_simp" (K (Config.Bool false));
+val debug_simp = Config.bool debug_simp_raw;
val trace_simp_default = Unsynchronized.ref false;
-val trace_simp_value = Config.declare "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
-val trace_simp = Config.bool trace_simp_value;
+val trace_simp_raw = Config.declare "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
+val trace_simp = Config.bool trace_simp_raw;
fun if_enabled (Simpset ({context, ...}, _)) flag f =
(case context of