# 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 *)