# HG changeset patch # User haftmann # Date 1224677747 -7200 # Node ID 98aba9fc90f617821968db15d513d8c5004f03d5 # Parent d89ac29171572a205cf45d7f5106b7c97eea19af added meet_sort_typ diff -r d89ac2917157 -r 98aba9fc90f6 src/Pure/sorts.ML --- a/src/Pure/sorts.ML Wed Oct 22 14:15:46 2008 +0200 +++ b/src/Pure/sorts.ML Wed Oct 22 14:15:47 2008 +0200 @@ -53,7 +53,9 @@ val class_error: Pretty.pp -> class_error -> string exception CLASS_ERROR of class_error val mg_domain: algebra -> string -> sort -> sort list (*exception CLASS_ERROR*) - val meet_sort: algebra -> typ * sort -> sort Vartab.table -> sort Vartab.table + val meet_sort: algebra -> typ * sort + -> sort Vartab.table -> sort Vartab.table (*exception CLASS_ERROR*) + val meet_sort_typ: algebra -> typ * sort -> typ -> typ (*exception CLASS_ERROR*) val of_sort: algebra -> typ * sort -> bool val weaken: algebra -> ('a * class -> class -> 'a) -> 'a * class -> class -> 'a val of_sort_derivation: Pretty.pp -> algebra -> @@ -365,6 +367,13 @@ | meet (Type (a, Ts)) S = fold2 meet Ts (mg_domain algebra a S); in uncurry meet end; +fun meet_sort_typ algebra (T, S) = + let + val tab = meet_sort algebra (T, S) Vartab.empty; + in Term.map_type_tvar (fn (v, _) => + TVar (v, (the o Vartab.lookup tab) v)) + end; + (* of_sort *)