src/Tools/Metis/src/Problem.sml

--- a/src/Tools/Metis/src/Problem.sml	Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Problem.sml	Thu Mar 24 17:49:27 2011 +0100
@@ -44,16 +44,16 @@
       Formula.listMkDisj (LiteralSet.transform Literal.toFormula cl);
 in
   fun toFormula prob =
-      Formula.listMkConj (map clauseToFormula (toClauses prob));
+      Formula.listMkConj (List.map clauseToFormula (toClauses prob));
 
   fun toGoal {axioms,conjecture} =
       let
         val clToFm = Formula.generalize o clauseToFormula
-        val clsToFm = Formula.listMkConj o map clToFm
+        val clsToFm = Formula.listMkConj o List.map clToFm
 
         val fm = Formula.False
         val fm =
-            if null conjecture then fm
+            if List.null conjecture then fm
             else Formula.Imp (clsToFm conjecture, fm)
         val fm = Formula.Imp (clsToFm axioms, fm)
       in
@@ -121,7 +121,7 @@
       val horn =
           if List.exists LiteralSet.null cls then Trivial
           else if List.all (fn cl => LiteralSet.size cl = 1) cls then Unit
-          else 
+          else
             let
               fun pos cl = LiteralSet.count Literal.positive cl <= 1
               fun neg cl = LiteralSet.count Literal.negative cl <= 1