src/Pure/goal.ML
changeset 19482 9f11af8f7ef9
parent 19423 51eeee99bd8f
child 19619 ee1104f972a4
--- 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" ^