src/Tools/Metis/src/Formula.sml

   fun isQuant [Term.Var _, _] = true
     | isQuant _ = false;
 
   fun promote (Term.Var v) = Atom (v,[])
     | promote (Term.Fn (f,tms)) =
-      if Name.equal f truthName andalso null tms then
+      if Name.equal f truthName andalso List.null tms then
         True
-      else if Name.equal f falsityName andalso null tms then
+      else if Name.equal f falsityName andalso List.null tms then
         False
       else if Name.toString f = !Term.negation andalso length tms = 1 then
         Not (promote (hd tms))
       else if Name.equal f conjunctionName andalso length tms = 2 then
         And (promote (hd tms), promote (List.nth (tms,1)))

 (* Splitting goals.                                                          *)
 (* ------------------------------------------------------------------------- *)
 
 local
   fun add_asms asms goal =
-      if null asms then goal else Imp (listMkConj (rev asms), goal);
+      if List.null asms then goal else Imp (listMkConj (rev asms), goal);
 
   fun add_var_asms asms v goal = add_asms asms (Forall (v,goal));
 
   fun split asms pol fm =
       case (pol,fm) of

       | (true, And (f1,f2)) => split asms true f1 @ split (f1 :: asms) true f2
       | (true, Or (f1,f2)) => split (Not f1 :: asms) true f2
       | (true, Imp (f1,f2)) => split (f1 :: asms) true f2
       | (true, Iff (f1,f2)) =>
         split (f1 :: asms) true f2 @ split (f2 :: asms) true f1
-      | (true, Forall (v,f)) => map (add_var_asms asms v) (split [] true f)
+      | (true, Forall (v,f)) => List.map (add_var_asms asms v) (split [] true f)
         (* Negative splittables *)
       | (false,False) => []
       | (false, Not f) => split asms true f
       | (false, And (f1,f2)) => split (f1 :: asms) false f2
       | (false, Or (f1,f2)) =>
         split asms false f1 @ split (Not f1 :: asms) false f2
       | (false, Imp (f1,f2)) => split asms true f1 @ split (f1 :: asms) false f2
       | (false, Iff (f1,f2)) =>
         split (f1 :: asms) false f2 @ split (f2 :: asms) false f1
-      | (false, Exists (v,f)) => map (add_var_asms asms v) (split [] false f)
+      | (false, Exists (v,f)) => List.map (add_var_asms asms v) (split [] false f)
         (* Unsplittables *)
       | _ => [add_asms asms (if pol then fm else Not fm)];
 in
   fun splitGoal fm = split [] true fm;
 end;