src/Pure/meta_simplifier.ML

--- a/src/Pure/meta_simplifier.ML	Fri Sep 03 15:54:03 2010 +0200
+++ b/src/Pure/meta_simplifier.ML	Fri Sep 03 16:09:12 2010 +0200
@@ -250,7 +250,7 @@
 
 (* simp depth *)
 
-val simp_depth_limit_value = Config.declare false "simp_depth_limit" (K (Config.Int 100));
+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 trace_simp_depth_limit = Unsynchronized.ref 1;
@@ -273,12 +273,11 @@
 
 exception SIMPLIFIER of string * thm;
 
-val debug_simp_value = Config.declare false "debug_simp" (K (Config.Bool false));
+val debug_simp_value = Config.declare "debug_simp" (K (Config.Bool false));
 val debug_simp = Config.bool debug_simp_value;
 
 val trace_simp_default = Unsynchronized.ref false;
-val trace_simp_value =
-  Config.declare false "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
+val trace_simp_value = Config.declare "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
 val trace_simp = Config.bool trace_simp_value;
 
 fun if_enabled (Simpset ({context, ...}, _)) flag f =