src/Tools/Metis/src/Normalize.sml

         SOME fm => fm
       | NONE => raise Bug "Normalize.lookupProved";
 
   fun prove acc proved ths =
       case ths of
-        [] => rev acc
+        [] => List.rev acc
       | th :: ths' =>
         if isProved proved th then prove acc proved ths'
         else
           let
             val pars = parentsThm th

 in
   fun proveCnf ths =
       let
         val (cls,_) = List.foldl add ([],initialCnf) ths
       in
-        rev cls
+        List.rev cls
       end;
 end;
 
 fun cnf fm =
     let