# HG changeset patch
# User wenzelm
# Date 1389135351 -3600
# Node ID 1276861f272437681907f5879ff3b4d7b25f0c62
# Parent  ed36358c20d56678cb672e1c2e531ad27c7b9f59
avoid hard tabs in output -- somewhat ill-defined;

diff -r ed36358c20d5 -r 1276861f2724 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Tue Jan 07 23:44:33 2014 +0100
+++ b/src/Provers/blast.ML	Tue Jan 07 23:55:51 2014 +0100
@@ -633,14 +633,14 @@
   in
       case topType thy t' of
           NONE   => stm   (*no type to attach*)
-        | SOME T => stm ^ "\t:: " ^ Syntax.string_of_typ ctxt T
+        | SOME T => stm ^ " :: " ^ Syntax.string_of_typ ctxt T
   end;
 
 
 (*Print tracing information at each iteration of prover*)
 fun trace_prover (State {ctxt, fullTrace, ...}) brs =
   let fun printPairs (((G,_)::_,_)::_)  = tracing (traceTerm ctxt G)
-        | printPairs (([],(H,_)::_)::_) = tracing (traceTerm ctxt H ^ "\t (Unsafe)")
+        | printPairs (([],(H,_)::_)::_) = tracing (traceTerm ctxt H ^ "  (Unsafe)")
         | printPairs _                 = ()
       fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
             (fullTrace := brs0 :: !fullTrace;
@@ -655,8 +655,8 @@
   if Config.get ctxt trace then
       (case !ntrail-ntrl of
             0 => ()
-          | 1 => tracing "\t1 variable UPDATED:"
-          | n => tracing ("\t" ^ string_of_int n ^ " variables UPDATED:");
+          | 1 => tracing " 1 variable UPDATED:"
+          | n => tracing (" " ^ string_of_int n ^ " variables UPDATED:");
        (*display the instantiations themselves, though no variable names*)
        List.app (fn v => tracing ("   " ^ string_of ctxt 4 (the (!v))))
            (List.take(!trail, !ntrail-ntrl));