src/Pure/goal.ML
changeset 19482 9f11af8f7ef9
parent 19423 51eeee99bd8f
child 19619 ee1104f972a4
     1.1 --- a/src/Pure/goal.ML	Thu Apr 27 12:11:56 2006 +0200
     1.2 +++ b/src/Pure/goal.ML	Thu Apr 27 15:06:35 2006 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4      val frees = Term.add_frees statement [];
     1.5      val fixed_frees = filter_out (member (op =) xs o #1) frees;
     1.6      val fixed_tfrees = fold (Term.add_tfreesT o #2) fixed_frees [];
     1.7 -    val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
     1.8 +    val params = map_filter (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
     1.9  
    1.10      fun err msg = cat_error msg
    1.11        ("The error(s) above occurred for the goal statement:\n" ^