diff -r 1b3115d1a8df -r 8d8c70b41bab src/FOLP/classical.ML
--- a/src/FOLP/classical.ML	Thu Mar 03 09:22:35 2005 +0100
+++ b/src/FOLP/classical.ML	Thu Mar 03 12:43:01 2005 +0100
@@ -112,7 +112,7 @@
 (*Note that allE precedes exI in haz_brls*)
 fun make_cs {safeIs,safeEs,hazIs,hazEs} =
   let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*)
-          partition (apl(0,op=) o subgoals_of_brl) 
+          List.partition (apl(0,op=) o subgoals_of_brl) 
              (sort (make_ord lessb) (joinrules(safeIs, safeEs)))
   in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs,
         safe0_brls=safe0_brls, safep_brls=safep_brls,