diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Pure/goal.ML	Thu Apr 27 15:06:35 2006 +0200
@@ -123,7 +123,7 @@
     val frees = Term.add_frees statement [];
     val fixed_frees = filter_out (member (op =) xs o #1) frees;
     val fixed_tfrees = fold (Term.add_tfreesT o #2) fixed_frees [];
-    val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
+    val params = map_filter (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
 
     fun err msg = cat_error msg
       ("The error(s) above occurred for the goal statement:\n" ^