handle Sorts.DOMAIN;
authorwenzelm
Wed Sep 29 13:52:01 1999 +0200 (1999-09-29)
changeset 7639538bd31709cb
parent 7638 f586d7995474
child 7640 6b7daae5d316
handle Sorts.DOMAIN;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Wed Sep 29 13:51:41 1999 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Wed Sep 29 13:52:01 1999 +0200
     1.3 @@ -247,14 +247,16 @@
     1.4        "Variable " ^ x ^ "::" ^ Sorts.str_of_sort S' ^ " not of sort " ^
     1.5          Sorts.str_of_sort S ^ ".";
     1.6  
     1.7 +    fun no_domain (a, c) = "No way to get " ^ a ^ "::" ^ c ^ ".";
     1.8 +
     1.9      fun meet (_, []) = ()
    1.10        | meet (Link (r as (ref (Param S'))), S) =
    1.11            if Sorts.sort_le classrel (S', S) then ()
    1.12            else r := mk_param (Sorts.inter_sort classrel (S', S))
    1.13        | meet (Link (ref T), S) = meet (T, S)
    1.14        | meet (PType (a, Ts), S) =
    1.15 -          seq2 meet (Ts, Sorts.mg_domain classrel arities a S
    1.16 -            handle TYPE (msg, _, _) => raise NO_UNIFIER msg)
    1.17 +          seq2 meet (Ts, Sorts.mg_domain (classrel, arities) a S
    1.18 +            handle Sorts.DOMAIN ac => raise NO_UNIFIER (no_domain ac))
    1.19        | meet (PTFree (x, S'), S) =
    1.20            if Sorts.sort_le classrel (S', S) then ()
    1.21            else raise NO_UNIFIER (not_in_sort x S' S)