1.1 --- a/src/Pure/sorts.ML	Wed Oct 22 14:15:46 2008 +0200
     1.2 +++ b/src/Pure/sorts.ML	Wed Oct 22 14:15:47 2008 +0200
     1.3 @@ -53,7 +53,9 @@
     1.4    val class_error: Pretty.pp -> class_error -> string
     1.5    exception CLASS_ERROR of class_error
     1.6    val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
     1.7 -  val meet_sort: algebra -> typ * sort -> sort Vartab.table -> sort Vartab.table
     1.8 +  val meet_sort: algebra -> typ * sort
     1.9 +    -> sort Vartab.table -> sort Vartab.table   (*exception CLASS_ERROR*)
    1.10 +  val meet_sort_typ: algebra -> typ * sort -> typ -> typ   (*exception CLASS_ERROR*)
    1.11    val of_sort: algebra -> typ * sort -> bool
    1.12    val weaken: algebra -> ('a * class -> class -> 'a) -> 'a * class -> class -> 'a
    1.13    val of_sort_derivation: Pretty.pp -> algebra ->
    1.14 @@ -365,6 +367,13 @@
    1.15        | meet (Type (a, Ts)) S = fold2 meet Ts (mg_domain algebra a S);
    1.16    in uncurry meet end;
    1.17  
    1.18 +fun meet_sort_typ algebra (T, S) =
    1.19 +  let
    1.20 +    val tab = meet_sort algebra (T, S) Vartab.empty;
    1.21 +  in Term.map_type_tvar (fn (v, _) =>
    1.22 +    TVar (v, (the o Vartab.lookup tab) v))
    1.23 +  end;
    1.24 +
    1.25  
    1.26  (* of_sort *)
    1.27