diff -r 9229d09363c0 -r 4ff1dc2aa18d src/Pure/unify.ML
--- a/src/Pure/unify.ML	Tue Aug 07 20:19:54 2007 +0200
+++ b/src/Pure/unify.ML	Tue Aug 07 20:19:55 2007 +0200
@@ -12,10 +12,14 @@
 
 signature UNIFY =
 sig
-  val trace_bound: int ref
-  val trace_simp: bool ref
-  val trace_types: bool ref
-  val search_bound: int ref
+  val trace_bound_value: Config.value Config.T
+  val trace_bound: int Config.T
+  val search_bound_value: Config.value Config.T
+  val search_bound: int Config.T
+  val trace_simp_value: Config.value Config.T
+  val trace_simp: bool Config.T
+  val trace_types_value: Config.value Config.T
+  val trace_types: bool Config.T
   val unifiers: theory * Envir.env * ((term * term) list) ->
     (Envir.env * (term * term) list) Seq.seq
   val smash_unifiers: theory -> (term * term) list -> Envir.env -> Envir.env Seq.seq
@@ -28,10 +32,22 @@
 
 (*Unification options*)
 
-val trace_bound = ref 25  (*tracing starts above this depth, 0 for full*)
-and search_bound = ref 30 (*unification quits above this depth*)
-and trace_simp = ref false  (*print dpairs before calling SIMPL*)
-and trace_types = ref false (*announce potential incompleteness of type unification*)
+(*tracing starts above this depth, 0 for full*)
+val trace_bound_value = Config.declare true "unify_trace_bound" (Config.Int 25);
+val trace_bound = Config.int trace_bound_value;
+
+(*unification quits above this depth*)
+val search_bound_value = Config.declare true "unify_search_bound" (Config.Int 30);
+val search_bound = Config.int search_bound_value;
+
+(*print dpairs before calling SIMPL*)
+val trace_simp_value = Config.declare true "unify_trace_simp" (Config.Bool false);
+val trace_simp = Config.bool trace_simp_value;
+
+(*announce potential incompleteness of type unification*)
+val trace_types_value = Config.declare true "unify_trace_types" (Config.Bool false);
+val trace_types = Config.bool trace_types_value;
+
 
 type binderlist = (string*typ) list;
 
@@ -318,8 +334,10 @@
   NB "vname" is only used in the call to make_args!!   *)
 fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs))
   : (term * (Envir.env * dpair list))Seq.seq =
-let (*Produce copies of uarg and cons them in front of uargs*)
-    fun copycons uarg (uargs, (env, dpairs)) =
+let
+  val trace_tps = Config.get_thy thy trace_types;
+  (*Produce copies of uarg and cons them in front of uargs*)
+  fun copycons uarg (uargs, (env, dpairs)) =
   Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
       (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),
      (env, dpairs)));
@@ -332,7 +350,7 @@
     (*attempt projection on argument with given typ*)
     val Ts = map (curry (fastype env) rbinder) targs;
     fun projenv (head, (Us,bary), targ, tail) =
-  let val env = if !trace_types then test_unify_types thy (base,bary,env)
+  let val env = if trace_tps then test_unify_types thy (base,bary,env)
           else unify_types thy (base,bary,env)
   in Seq.make (fn () =>
       let val (env',args) = make_args vname (Ts,env,Us);
@@ -551,26 +569,30 @@
   SIMPL may raise exception CANTUNIFY. *)
 fun hounifiers (thy,env, tus : (term*term)list)
   : (Envir.env * (term*term)list)Seq.seq =
-  let fun add_unify tdepth ((env,dpairs), reseq) =
+  let
+    val trace_bnd = Config.get_thy thy trace_bound;
+    val search_bnd = Config.get_thy thy search_bound;
+    val trace_smp = Config.get_thy thy trace_simp;
+    fun add_unify tdepth ((env,dpairs), reseq) =
     Seq.make (fn()=>
     let val (env',flexflex,flexrigid) =
-         (if tdepth> !trace_bound andalso !trace_simp
+         (if tdepth> trace_bnd andalso trace_smp
     then print_dpairs thy "Enter SIMPL" (env,dpairs)  else ();
     SIMPL thy (env,dpairs))
     in case flexrigid of
         [] => SOME (List.foldr (add_ffpair thy) (env',[]) flexflex, reseq)
       | dp::frigid' =>
-    if tdepth > !search_bound then
+    if tdepth > search_bnd then
         (warning "Unification bound exceeded"; Seq.pull reseq)
     else
-    (if tdepth > !trace_bound then
+    (if tdepth > trace_bnd then
         print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
      else ();
      Seq.pull (Seq.it_right (add_unify (tdepth+1))
          (MATCH thy (env',dp, frigid'@flexflex), reseq)))
     end
     handle CANTUNIFY =>
-      (if tdepth > !trace_bound then tracing"Failure node" else ();
+      (if tdepth > trace_bnd then tracing"Failure node" else ();
        Seq.pull reseq));
      val dps = map (fn(t,u)=> ([],t,u)) tus
   in add_unify 1 ((env, dps), Seq.empty) end;