src/Pure/sorts.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 16399 0c9265f1ce31
     1.1 --- a/src/Pure/sorts.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/sorts.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -133,7 +133,7 @@
     1.4  fun norm_sort _ [] = []
     1.5    | norm_sort _ (S as [_]) = S
     1.6    | norm_sort classes S =
     1.7 -      sort_strings (distinct_class (filter (minimal_class classes S) S));
     1.8 +      sort_strings (distinct_class (List.filter (minimal_class classes S) S));
     1.9  
    1.10  end;
    1.11  
    1.12 @@ -161,7 +161,7 @@
    1.13    in intr S end;
    1.14  
    1.15  (*instersect sorts (preserves minimality)*)
    1.16 -fun inter_sort classes = sort_strings o foldr (inter_class classes);
    1.17 +fun inter_sort classes = sort_strings o Library.foldr (inter_class classes);
    1.18  
    1.19  
    1.20  
    1.21 @@ -179,7 +179,7 @@
    1.22              NONE => raise DOMAIN (a, c)
    1.23            | SOME Ss => Ss);
    1.24          val doms = map mg_dom S;
    1.25 -      in foldl (ListPair.map (inter_sort classes)) (hd doms, tl doms) end;
    1.26 +      in Library.foldl (ListPair.map (inter_sort classes)) (hd doms, tl doms) end;
    1.27  
    1.28  
    1.29  (* of_sort *)
    1.30 @@ -231,8 +231,8 @@
    1.31                  witn_types path ts (solved_failed, S)
    1.32                else
    1.33                  let val ((solved', failed'), ws) = witn_sorts (S :: path) (solved_failed, SS) in
    1.34 -                  if forall is_some ws then
    1.35 -                    let val w = (Type (t, map (#1 o the) ws), S)
    1.36 +                  if forall isSome ws then
    1.37 +                    let val w = (Type (t, map (#1 o valOf) ws), S)
    1.38                      in ((w :: solved', failed'), SOME w) end
    1.39                    else witn_types path ts ((solved', failed'), S)
    1.40                  end
    1.41 @@ -252,7 +252,7 @@
    1.42        | check_result (SOME (T, S)) =
    1.43            if of_sort (classes, arities) (T, S) then SOME (T, S)
    1.44            else sys_error ("Sorts.witness_sorts: bad witness for sort " ^ str_of_sort S);
    1.45 -  in mapfilter check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end;
    1.46 +  in List.mapPartial check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end;
    1.47  
    1.48  end;
    1.49