src/Pure/unify.ML

 *)
 
 signature UNIFY =
 sig
   val search_bound: int Config.T
+  val unify_trace: bool Config.T
   val unify_trace_bound: int Config.T
   val unify_trace_simp: bool Config.T
   val unify_trace_types: bool Config.T
   val hounifiers: (string * typ) list -> Context.generic * Envir.env * ((term * term) list) ->
     (Envir.env * (term * term) list) Seq.seq

 val search_bound = Config.declare_int ("unify_search_bound", \<^here>) (K 60);
 
 
 (* diagnostics *)
 
+val unify_trace = Config.declare_bool ("unify_trace", \<^here>) (K false);
+
 (*tracing starts above this depth, 0 for full*)
 val unify_trace_bound = Config.declare_int ("unify_trace_bound", \<^here>) (K 50);
 
 (*print dpairs before calling SIMPL*)
 val unify_trace_simp = Config.declare_bool ("unify_trace_simp", \<^here>) (K false);
 
 (*announce potential incompleteness of type unification*)
 val unify_trace_types = Config.declare_bool ("unify_trace_types", \<^here>) (K false);
+
+fun cond_tracing ctxt msg =
+  if Config.get_generic ctxt unify_trace andalso Context_Position.is_visible_generic ctxt then
+    tracing (msg ())
+  else ();
 
 
 type binderlist = (string * typ) list;
 
 type dpair = binderlist * term * term;

 fun unify_types context TU env =
   Pattern.unify_types context TU env handle Pattern.Unif => raise CANTUNIFY;
 
 fun test_unify_types context (T, U) env =
   let
-    fun trace () =
-      if Context_Position.is_visible_generic context then
-        let val str_of = Syntax.string_of_typ (Context.proof_of context)
-        in tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T) end
-      else ();
+    fun msg () =
+      let val str_of = Syntax.string_of_typ (Context.proof_of context)
+      in "Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T end
     val env' = unify_types context (T, U) env;
-  in if is_TVar T orelse is_TVar U then trace () else (); env' end;
+  in if is_TVar T orelse is_TVar U then cond_tracing context msg else (); env' end;
 
 (*Is the term eta-convertible to a single variable with the given rbinder?
   Examples: ?a   ?f(B.0)   ?g(B.1,B.0)
   Result is var a for use in SIMPL. *)
 fun get_eta_var ([], _, Var vT) = vT

 
 (*Print a tracing message + list of dpairs.
   In t \<equiv> u print u first because it may be rigid or flexible --
     t is always flexible.*)
 fun print_dpairs context msg (env, dpairs) =
-  if Context_Position.is_visible_generic context then
-    let
-      fun pdp (rbinder, t, u) =
-        let
-          val ctxt = Context.proof_of context;
-          fun termT t =
-            Syntax.pretty_term ctxt (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
-          val prt = Pretty.blk (0, [termT u, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, termT t]);
-        in tracing (Pretty.string_of prt) end;
-    in tracing msg; List.app pdp dpairs end
-  else ();
+  let
+    fun pdp (rbinder, t, u) =
+      let
+        val ctxt = Context.proof_of context;
+        fun termT t =
+          Syntax.pretty_term ctxt (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
+        val prt = Pretty.blk (0, [termT u, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, termT t]);
+      in Pretty.string_of prt end;
+  in
+    cond_tracing context (fn () => msg);
+    List.app (fn dp => cond_tracing context (fn () => pdp dp)) dpairs
+  end;
 
 
 (*Unify the dpairs in the environment.
   Returns flex-flex disagreement pairs NOT IN normal form.
   SIMPL may raise exception CANTUNIFY. *)

         in
           (case flexrigid of
             [] => SOME (fold_rev (add_ffpair context) flexflex (env', []), reseq)
           | dp :: frigid' =>
               if tdepth > search_bound then
-                (if Context_Position.is_visible_generic context
-                 then warning "Unification bound exceeded" else (); Seq.pull reseq)
+                (if Context_Position.is_visible_generic context then
+                   warning "Unification bound exceeded -- see unify trace for details"
+                 else (); Seq.pull reseq)
               else
                (if tdepth > unify_trace_bound then
                   print_dpairs context "Enter MATCH" (env',flexrigid@flexflex)
                 else ();
                 Seq.pull (Seq.it_right
                     (add_unify (tdepth + 1)) (MATCH context (env',dp, frigid'@flexflex), reseq))))
         end
         handle CANTUNIFY =>
-         (if tdepth > unify_trace_bound andalso Context_Position.is_visible_generic context
-          then tracing "Failure node"
+         (if tdepth > unify_trace_bound
+          then cond_tracing context (fn () => "Failure node")
           else (); Seq.pull reseq));
     val dps = map (fn (t, u) => (binders, t, u)) tus;
   in add_unify 1 ((env, dps), Seq.empty) end;
 
 fun unifiers (params as (context, env, tus)) =