1.1 --- a/src/Provers/blast.ML	Tue Jan 07 23:44:33 2014 +0100
     1.2 +++ b/src/Provers/blast.ML	Tue Jan 07 23:55:51 2014 +0100
     1.3 @@ -633,14 +633,14 @@
     1.4    in
     1.5        case topType thy t' of
     1.6            NONE   => stm   (*no type to attach*)
     1.7 -        | SOME T => stm ^ "\t:: " ^ Syntax.string_of_typ ctxt T
     1.8 +        | SOME T => stm ^ " :: " ^ Syntax.string_of_typ ctxt T
     1.9    end;
    1.10  
    1.11  
    1.12  (*Print tracing information at each iteration of prover*)
    1.13  fun trace_prover (State {ctxt, fullTrace, ...}) brs =
    1.14    let fun printPairs (((G,_)::_,_)::_)  = tracing (traceTerm ctxt G)
    1.15 -        | printPairs (([],(H,_)::_)::_) = tracing (traceTerm ctxt H ^ "\t (Unsafe)")
    1.16 +        | printPairs (([],(H,_)::_)::_) = tracing (traceTerm ctxt H ^ "  (Unsafe)")
    1.17          | printPairs _                 = ()
    1.18        fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
    1.19              (fullTrace := brs0 :: !fullTrace;
    1.20 @@ -655,8 +655,8 @@
    1.21    if Config.get ctxt trace then
    1.22        (case !ntrail-ntrl of
    1.23              0 => ()
    1.24 -          | 1 => tracing "\t1 variable UPDATED:"
    1.25 -          | n => tracing ("\t" ^ string_of_int n ^ " variables UPDATED:");
    1.26 +          | 1 => tracing " 1 variable UPDATED:"
    1.27 +          | n => tracing (" " ^ string_of_int n ^ " variables UPDATED:");
    1.28         (*display the instantiations themselves, though no variable names*)
    1.29         List.app (fn v => tracing ("   " ^ string_of ctxt 4 (the (!v))))
    1.30             (List.take(!trail, !ntrail-ntrl));