src/Provers/blast.ML
changeset 30190 479806475f3c
parent 30187 b92b3375e919
child 30242 aea5d7fa7ef5
--- a/src/Provers/blast.ML	Sun Mar 01 16:48:06 2009 +0100
+++ b/src/Provers/blast.ML	Sun Mar 01 23:36:12 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 ();
@@ -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*)