src/Pure/meta_simplifier.ML

   setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler
   setloop' setloop addloop addloop' delloop setSSolver addSSolver setSolver addSolver;
 
 signature BASIC_META_SIMPLIFIER =
 sig
-  val debug_simp: bool Unsynchronized.ref
-  val trace_simp: bool Unsynchronized.ref
+  val debug_simp: bool Config.T
+  val debug_simp_value: Config.value Config.T
+  val trace_simp: bool Config.T
+  val trace_simp_value: Config.value Config.T
   val trace_simp_depth_limit: int Unsynchronized.ref
   type rrule
   val eq_rrule: rrule * rrule -> bool
   type simpset
   type proc

 
 (* diagnostics *)
 
 exception SIMPLIFIER of string * thm;
 
-val debug_simp = Unsynchronized.ref false;
-val trace_simp = Unsynchronized.ref false;
+val debug_simp_value = Config.declare false "debug_simp" (Config.Bool false);
+val debug_simp = Config.bool debug_simp_value;
+
+val trace_simp_value = Config.declare false "trace_simp" (Config.Bool false);
+val trace_simp = Config.bool trace_simp_value;
 
 local
 
 fun prnt ss warn a = if warn then warning a else trace_depth ss a;
 

     val names = Term.declare_term_names t Name.context;
     val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
     fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
   in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
 
+fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
+  Syntax.string_of_term ctxt
+    (if Config.get ctxt debug_simp then t else show_bounds ss t));
+
 in
 
-fun print_term ss warn a thy t = prnt ss warn (a ^ "\n" ^
-  Syntax.string_of_term_global thy (if ! debug_simp then t else show_bounds ss t));
-
-fun debug warn a ss = if ! debug_simp then prnt ss warn (a ()) else ();
-fun trace warn a ss = if ! trace_simp then prnt ss warn (a ()) else ();
-
-fun debug_term warn a ss thy t = if ! debug_simp then print_term ss warn (a ()) thy t else ();
-fun trace_term warn a ss thy t = if ! trace_simp then print_term ss warn (a ()) thy t else ();
+fun print_term_global ss warn a thy t =
+  print_term ss warn (K a) t (ProofContext.init thy);
+
+fun if_enabled (Simpset ({context, ...}, _)) flag f =
+  (case context of
+    SOME ctxt => if Config.get ctxt flag then f ctxt else ()
+  | NONE => ())
+
+fun debug warn a ss = if_enabled ss debug_simp (fn _ => prnt ss warn (a ()));
+fun trace warn a ss = if_enabled ss trace_simp (fn _ => prnt ss warn (a ()));
+
+fun debug_term warn a ss t = if_enabled ss debug_simp (print_term ss warn a t);
+fun trace_term warn a ss t = if_enabled ss trace_simp (print_term ss warn a t);
 
 fun trace_cterm warn a ss ct =
-  if ! trace_simp then print_term ss warn (a ()) (Thm.theory_of_cterm ct) (Thm.term_of ct)
-  else ();
+  if_enabled ss trace_simp (print_term ss warn a (Thm.term_of ct));
 
 fun trace_thm a ss th =
-  if ! trace_simp then print_term ss false (a ()) (Thm.theory_of_thm th) (Thm.full_prop_of th)
-  else ();
+  if_enabled ss trace_simp (print_term ss false a (Thm.full_prop_of th));
 
 fun trace_named_thm a ss (th, name) =
-  if ! trace_simp then
-    print_term ss false (if name = "" then a () else a () ^ " " ^ quote name ^ ":")
-      (Thm.theory_of_thm th) (Thm.full_prop_of th)
-  else ();
+  if_enabled ss trace_simp (print_term ss false
+    (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
+    (Thm.full_prop_of th));
 
 fun warn_thm a ss th =
-  print_term ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th);
+  print_term_global ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th);
 
 fun cond_warn_thm a (ss as Simpset ({context, ...}, _)) th =
   if is_some context then () else warn_thm a ss th;
 
 end;

     let
       val thy = Thm.theory_of_thm thm;
       val _ $ _ $ prop0 = Thm.prop_of thm;
     in
       trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
-      trace_term false (fn () => "Should have proved:") ss thy prop0;
+      trace_term false (fn () => "Should have proved:") ss prop0;
       NONE
     end;
 
 
 (* mk_procrule *)

     in sort rrs ([],[]) end
 
     fun proc_rews [] = NONE
       | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
           if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then
-            (debug_term false (fn () => "Trying procedure " ^ quote name ^ " on:") ss thyt eta_t;
+            (debug_term false (fn () => "Trying procedure " ^ quote name ^ " on:") ss eta_t;
              case proc ss eta_t' of
                NONE => (debug false (fn () => "FAILED") ss; proc_rews ps)
              | SOME raw_thm =>
                  (trace_thm (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:")
                    ss raw_thm;

           if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
           then insert (op =) x else I
         | _ => I) (term_of ct) [];
     in
       if null bs then ()
-      else print_term ss true ("Simplifier: term contains loose bounds: " ^ commas_quote bs)
+      else print_term_global ss true ("Simplifier: term contains loose bounds: " ^ commas_quote bs)
         (Thm.theory_of_cterm ct) (Thm.term_of ct)
     end
   else ();
 
 fun rewrite_cterm mode prover raw_ss raw_ct =