proper configuration options Proof_Context.debug and Proof_Context.verbose;
discontinued alias Proof.verbose = Proof_Context.verbose;

--- a/src/Pure/Isar/proof.ML	Thu May 12 16:00:48 2011 +0200
+++ b/src/Pure/Isar/proof.ML	Thu May 12 16:23:13 2011 +0200
@@ -31,7 +31,6 @@
   val assert_no_chain: state -> state
   val enter_forward: state -> state
   val goal_message: (unit -> Pretty.T) -> state -> state
-  val verbose: bool Unsynchronized.ref
   val pretty_state: int -> state -> Pretty.T list
   val pretty_goals: bool -> state -> Pretty.T list
   val refine: Method.text -> state -> state Seq.seq
@@ -324,8 +323,6 @@
 
 (** pretty_state **)
 
-val verbose = Proof_Context.verbose;
-
 fun pretty_facts _ _ NONE = []
   | pretty_facts s ctxt (SOME ths) =
       [Pretty.big_list (s ^ "this:") (map (Display.pretty_thm ctxt) ths), Pretty.str ""];
@@ -333,6 +330,7 @@
 fun pretty_state nr state =
   let
     val {context = ctxt, facts, mode, goal = _} = current state;
+    val verbose = Config.get ctxt Proof_Context.verbose;
 
     fun levels_up 0 = ""
       | levels_up 1 = "1 level up"
@@ -357,15 +355,15 @@
       | prt_goal NONE = [];
 
     val prt_ctxt =
-      if ! verbose orelse mode = Forward then Proof_Context.pretty_context ctxt
+      if verbose orelse mode = Forward then Proof_Context.pretty_context ctxt
       else if mode = Backward then Proof_Context.pretty_ctxt ctxt
       else [];
   in
     [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
-      (if ! verbose then ", depth " ^ string_of_int (level state div 2 - 1) else "")),
+      (if verbose then ", depth " ^ string_of_int (level state div 2 - 1) else "")),
       Pretty.str ""] @
     (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
-    (if ! verbose orelse mode = Forward then
+    (if verbose orelse mode = Forward then
        pretty_facts "" ctxt facts @ prt_goal (try find_goal state)
      else if mode = Chain then pretty_facts "picking " ctxt facts
      else prt_goal (try find_goal state))

--- a/src/Pure/Isar/proof_context.ML	Thu May 12 16:00:48 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu May 12 16:23:13 2011 +0200
@@ -151,8 +151,8 @@
   val print_binds: Proof.context -> unit
   val print_lthms: Proof.context -> unit
   val print_cases: Proof.context -> unit
-  val debug: bool Unsynchronized.ref
-  val verbose: bool Unsynchronized.ref
+  val debug: bool Config.T
+  val verbose: bool Config.T
   val pretty_ctxt: Proof.context -> Pretty.T list
   val pretty_context: Proof.context -> Pretty.T list
 end;
@@ -1235,11 +1235,11 @@
 
 (* core context *)
 
-val debug = Unsynchronized.ref false;
-val verbose = Unsynchronized.ref false;
+val debug = Config.bool (Config.declare "Proof_Context.debug" (K (Config.Bool false)));
+val verbose = Config.bool (Config.declare "Proof_Context.verbose" (K (Config.Bool false)));
 
 fun pretty_ctxt ctxt =
-  if not (! debug) then []
+  if not (Config.get ctxt debug) then []
   else
     let
       val prt_term = Syntax.pretty_term ctxt;
@@ -1275,8 +1275,8 @@
 
 fun pretty_context ctxt =
   let
-    val is_verbose = ! verbose;
-    fun verb f x = if is_verbose then f (x ()) else [];
+    val verbose = Config.get ctxt verbose;
+    fun verb f x = if verbose then f (x ()) else [];
 
     val prt_term = Syntax.pretty_term ctxt;
     val prt_typ = Syntax.pretty_typ ctxt;

--- a/src/Pure/Isar/proof_display.ML	Thu May 12 16:00:48 2011 +0200
+++ b/src/Pure/Isar/proof_display.ML	Thu May 12 16:23:13 2011 +0200
@@ -27,7 +27,7 @@
 (* toplevel pretty printing *)
 
 fun pp_context ctxt =
- (if ! Proof_Context.debug then
+ (if Config.get ctxt Proof_Context.debug then
     Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
   else Pretty.str "<context>");