1.1 --- a/src/Pure/unify.ML	Thu Jul 18 20:53:22 2013 +0200
     1.2 +++ b/src/Pure/unify.ML	Thu Jul 18 21:06:21 2013 +0200
     1.3 @@ -332,7 +332,7 @@
     1.4    let
     1.5      fun mc (rbinder, targs, u, ed as (env, dpairs)) : (term * (Envir.env * dpair list)) Seq.seq =
     1.6        let
     1.7 -        val trace_tps = Config.get_global thy trace_types;
     1.8 +        val trace_types = Config.get_global thy trace_types;
     1.9          (*Produce copies of uarg and cons them in front of uargs*)
    1.10          fun copycons uarg (uargs, (env, dpairs)) =
    1.11            Seq.map (fn (uarg', ed') => (uarg' :: uargs, ed'))
    1.12 @@ -349,7 +349,7 @@
    1.13          fun projenv (head, (Us, bary), targ, tail) =
    1.14            let
    1.15              val env =
    1.16 -              if trace_tps then test_unify_types thy (base, bary) env
    1.17 +              if trace_types then test_unify_types thy (base, bary) env
    1.18                else unify_types thy (base, bary) env
    1.19            in
    1.20              Seq.make (fn () =>
    1.21 @@ -587,31 +587,31 @@
    1.22    SIMPL may raise exception CANTUNIFY. *)
    1.23  fun hounifiers (thy, env, tus : (term * term) list) : (Envir.env * (term * term) list) Seq.seq =
    1.24    let
    1.25 -    val trace_bnd = Config.get_global thy trace_bound;
    1.26 -    val search_bnd = Config.get_global thy search_bound;
    1.27 -    val trace_smp = Config.get_global thy trace_simp;
    1.28 +    val trace_bound = Config.get_global thy trace_bound;
    1.29 +    val search_bound = Config.get_global thy search_bound;
    1.30 +    val trace_simp = Config.get_global thy trace_simp;
    1.31      fun add_unify tdepth ((env, dpairs), reseq) =
    1.32        Seq.make (fn () =>
    1.33          let
    1.34            val (env', flexflex, flexrigid) =
    1.35 -           (if tdepth > trace_bnd andalso trace_smp
    1.36 +           (if tdepth > trace_bound andalso trace_simp
    1.37              then print_dpairs thy "Enter SIMPL" (env, dpairs) else ();
    1.38              SIMPL thy (env, dpairs));
    1.39          in
    1.40            (case flexrigid of
    1.41              [] => SOME (fold_rev (add_ffpair thy) flexflex (env', []), reseq)
    1.42            | dp :: frigid' =>
    1.43 -              if tdepth > search_bnd then
    1.44 +              if tdepth > search_bound then
    1.45                  (warning "Unification bound exceeded"; Seq.pull reseq)
    1.46                else
    1.47 -               (if tdepth > trace_bnd then
    1.48 +               (if tdepth > trace_bound then
    1.49                    print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
    1.50                  else ();
    1.51                  Seq.pull (Seq.it_right
    1.52                      (add_unify (tdepth + 1)) (MATCH thy (env',dp, frigid'@flexflex), reseq))))
    1.53          end
    1.54          handle CANTUNIFY =>
    1.55 -         (if tdepth > trace_bnd then tracing"Failure node" else ();
    1.56 +         (if tdepth > trace_bound then tracing "Failure node" else ();
    1.57            Seq.pull reseq));
    1.58      val dps = map (fn (t, u) => ([], t, u)) tus;
    1.59    in add_unify 1 ((env, dps), Seq.empty) end;