src/Provers/blast.ML

--- a/src/Provers/blast.ML	Wed Mar 04 10:43:39 2009 +0100
+++ b/src/Provers/blast.ML	Wed Mar 04 10:45:52 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Provers/blast.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
 
@@ -764,8 +763,8 @@
             end
       (*substitute throughout "stack frame"; extract affected formulae*)
       fun subFrame ((Gs,Hs), (changed, frames)) =
-            let val (changed', Gs') = foldr subForm (changed, []) Gs
-                val (changed'', Hs') = foldr subForm (changed', []) Hs
+            let val (changed', Gs') = List.foldr subForm (changed, []) Gs
+                val (changed'', Hs') = List.foldr subForm (changed', []) Hs
             in  (changed'', (Gs',Hs')::frames)  end
       (*substitute throughout literals; extract affected ones*)
       fun subLit (lit, (changed, nlits)) =
@@ -773,8 +772,8 @@
             in  if nlit aconv lit then (changed, nlit::nlits)
                                   else ((nlit,true)::changed, nlits)
             end
-      val (changed, lits') = foldr subLit ([], []) lits
-      val (changed', pairs') = foldr subFrame (changed, []) pairs
+      val (changed, lits') = List.foldr subLit ([], []) lits
+      val (changed', pairs') = List.foldr subFrame (changed, []) pairs
   in  if !trace then writeln ("Substituting " ^ traceTerm thy u ^
                               " for " ^ traceTerm thy t ^ " in branch" )
       else ();
@@ -913,7 +912,7 @@
 
 fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) =
   if b then
-    writeln (end_timing start ^ " for search.  Closed: "
+    writeln (#message (end_timing start) ^ " for search.  Closed: "
              ^ Int.toString (!nclosed) ^
              " tried: " ^ Int.toString (!ntried) ^
              " tactics: " ^ Int.toString (length tacs))
@@ -971,7 +970,7 @@
                                     then lim - (1+log(length rules))
                                     else lim   (*discourage branching updates*)
                          val vars  = vars_in_vars vars
-                         val vars' = foldr add_terms_vars vars prems
+                         val vars' = List.foldr add_terms_vars vars prems
                          val choices' = (ntrl, nbrs, PRV) :: choices
                          val tacs' = (tac(updated,false,true))
                                      :: tacs  (*no duplication; rotate*)
@@ -1098,7 +1097,7 @@
                     then
                      let val updated = ntrl < !ntrail (*branch updated*)
                          val vars  = vars_in_vars vars
-                         val vars' = foldr add_terms_vars vars prems
+                         val vars' = List.foldr add_terms_vars vars prems
                             (*duplicate H if md permits*)
                          val dup = md (*earlier had "andalso vars' <> vars":
                                   duplicate only if the subgoal has new vars*)
@@ -1264,7 +1263,7 @@
                        else ();
                        backtrack choices)
             | cell => (if (!trace orelse !stats)
-                       then writeln (end_timing start ^ " for reconstruction")
+                       then writeln (#message (end_timing start) ^ " for reconstruction")
                        else ();
                        Seq.make(fn()=> cell))
           end