# HG changeset patch
# User wenzelm
# Date 861357518 -7200
# Node ID d9f6299dbf9f949f447deac076e2b227a8115173
# Parent  271062b8c461d43b3cb1604eef5351c8d2d115cd
tuned check_has_sort;
fixed norm_typ: also does norm_sort;

diff -r 271062b8c461 -r d9f6299dbf9f src/Pure/type.ML
--- a/src/Pure/type.ML	Fri Apr 18 11:57:51 1997 +0200
+++ b/src/Pure/type.ML	Fri Apr 18 11:58:38 1997 +0200
@@ -269,8 +269,8 @@
 
 
 fun check_has_sort (TySg {classrel, arities, ...}, T, S) =
-  if Sorts.sort_le classrel ((Sorts.least_sort classrel arities T), S) then ()
-  else raise TYPE ("Type not of sort " ^ Sorts.str_of_sort S, [T], []);
+  if Sorts.of_sort classrel arities (T, S) then ()
+  else raise_type ("Type not of sort " ^ Sorts.str_of_sort S) [T] [];
 
 
 (*Instantiation of type variables in types *)
@@ -287,18 +287,19 @@
 
 (* norm_typ *)
 
-fun norm_typ (TySg {abbrs, ...}) ty =
+(*expand abbreviations and normalize sorts*)
+fun norm_typ (tsig as TySg {abbrs, ...}) ty =
   let
     val idx = maxidx_of_typ ty + 1;
 
-    fun expand (Type (a, Ts)) =
+    fun norm (Type (a, Ts)) =
           (case assoc (abbrs, a) of
-            Some (vs, U) =>
-              expand (inst_typ (map (rpair idx) vs ~~ Ts) (incr_tvar idx U))
-          | None => Type (a, map expand Ts))
-      | expand T = T
+            Some (vs, U) => norm (inst_typ (map (rpair idx) vs ~~ Ts) (incr_tvar idx U))
+          | None => Type (a, map norm Ts))
+      | norm (TFree (x, S)) = TFree (x, norm_sort tsig S)
+      | norm (TVar (xi, S)) = TVar (xi, norm_sort tsig S);
   in
-    expand ty
+    norm ty
   end;