# 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;