# HG changeset patch
# User wenzelm
# Date 1414838455 -3600
# Node ID d5ff8b782b294eb37b3027ad27678e62c9188bb7
# Parent  cc1e03929685b16c46378ff6e0c0afb75cc7452b
eliminated former Proof General preferences;

diff -r cc1e03929685 -r d5ff8b782b29 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri Oct 31 23:51:54 2014 +0100
+++ b/src/Pure/pattern.ML	Sat Nov 01 11:40:55 2014 +0100
@@ -12,7 +12,6 @@
 
 signature PATTERN =
 sig
-  val unify_trace_failure_default: bool Unsynchronized.ref
   val unify_trace_failure_raw: Config.raw
   val unify_trace_failure: bool Config.T
   val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
@@ -40,10 +39,8 @@
 exception Unif;
 exception Pattern;
 
-val unify_trace_failure_default = Unsynchronized.ref false;
 val unify_trace_failure_raw =
-  Config.declare_global ("unify_trace_failure", @{here})
-    (fn _ => Config.Bool (! unify_trace_failure_default));
+  Config.declare_global ("unify_trace_failure", @{here}) (fn _ => Config.Bool false);
 val unify_trace_failure = Config.bool unify_trace_failure_raw;
 
 fun string_of_term thy env binders t =
diff -r cc1e03929685 -r d5ff8b782b29 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Fri Oct 31 23:51:54 2014 +0100
+++ b/src/Pure/raw_simplifier.ML	Sat Nov 01 11:40:55 2014 +0100
@@ -110,8 +110,6 @@
   val simproc_global: theory -> string -> string list ->
     (Proof.context -> 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 -> Proof.context -> Proof.context
@@ -397,10 +395,8 @@
 val simp_depth_limit_raw = Config.declare ("simp_depth_limit", @{here}) (K (Config.Int 100));
 val simp_depth_limit = Config.int simp_depth_limit_raw;
 
-val simp_trace_depth_limit_default = Unsynchronized.ref 1;
 val simp_trace_depth_limit_raw =
-  Config.declare ("simp_trace_depth_limit", @{here})
-    (fn _ => Config.Int (! simp_trace_depth_limit_default));
+  Config.declare ("simp_trace_depth_limit", @{here}) (fn _ => Config.Int 1);
 val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw;
 
 fun inc_simp_depth ctxt =
@@ -422,9 +418,7 @@
 val simp_debug_raw = Config.declare ("simp_debug", @{here}) (K (Config.Bool false));
 val simp_debug = Config.bool simp_debug_raw;
 
-val simp_trace_default = Unsynchronized.ref false;
-val simp_trace_raw =
-  Config.declare ("simp_trace", @{here}) (fn _ => Config.Bool (! simp_trace_default));
+val simp_trace_raw = Config.declare ("simp_trace", @{here}) (fn _ => Config.Bool false);
 val simp_trace = Config.bool simp_trace_raw;
 
 fun cond_warning ctxt msg =