# HG changeset patch
# User wenzelm
# Date 938605921 -7200
# Node ID 538bd31709cb547491a5cfb399e429bfcb47d023
# Parent  f586d7995474c57a7e5a73ad3c1c97dd402fe1e2
handle Sorts.DOMAIN;

diff -r f586d7995474 -r 538bd31709cb src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Wed Sep 29 13:51:41 1999 +0200
+++ b/src/Pure/type_infer.ML	Wed Sep 29 13:52:01 1999 +0200
@@ -247,14 +247,16 @@
       "Variable " ^ x ^ "::" ^ Sorts.str_of_sort S' ^ " not of sort " ^
         Sorts.str_of_sort S ^ ".";
 
+    fun no_domain (a, c) = "No way to get " ^ a ^ "::" ^ c ^ ".";
+
     fun meet (_, []) = ()
       | meet (Link (r as (ref (Param S'))), S) =
           if Sorts.sort_le classrel (S', S) then ()
           else r := mk_param (Sorts.inter_sort classrel (S', S))
       | meet (Link (ref T), S) = meet (T, S)
       | meet (PType (a, Ts), S) =
-          seq2 meet (Ts, Sorts.mg_domain classrel arities a S
-            handle TYPE (msg, _, _) => raise NO_UNIFIER msg)
+          seq2 meet (Ts, Sorts.mg_domain (classrel, arities) a S
+            handle Sorts.DOMAIN ac => raise NO_UNIFIER (no_domain ac))
       | meet (PTFree (x, S'), S) =
           if Sorts.sort_le classrel (S', S) then ()
           else raise NO_UNIFIER (not_in_sort x S' S)