src/Pure/type.ML
changeset 16650 bd4f7149ba1e
parent 16444 80c8f742c6fc
child 16885 cabcd33cde18
     1.1 --- a/src/Pure/type.ML	Fri Jul 01 14:18:27 2005 +0200
     1.2 +++ b/src/Pure/type.ML	Fri Jul 01 14:19:36 2005 +0200
     1.3 @@ -56,6 +56,7 @@
     1.4    exception TUNIFY
     1.5    val unify: tsig -> tyenv * int -> typ * typ -> tyenv * int
     1.6    val raw_unify: typ * typ -> bool
     1.7 +  val eq_type: tyenv -> typ * typ -> bool
     1.8  
     1.9    (*extend and merge type signatures*)
    1.10    val add_classes: Pretty.pp -> NameSpace.naming -> (bstring * class list) list -> tsig -> tsig
    1.11 @@ -388,6 +389,13 @@
    1.12    (unify empty_tsig (Vartab.empty, 0) (strip_sorts ty1, strip_sorts ty2); true)
    1.13      handle TUNIFY => false;
    1.14  
    1.15 +(*check whether two types are equal with respect to a type environment*)
    1.16 +fun eq_type tye (T, T') =
    1.17 +  (case (devar (T, tye), devar (T', tye)) of
    1.18 +     (Type (s, Ts), Type (s', Ts')) =>
    1.19 +       s = s' andalso ListPair.all (eq_type tye) (Ts, Ts')
    1.20 +   | (U, U') => U = U');
    1.21 +
    1.22  
    1.23  
    1.24  (** extend and merge type signatures **)