--- a/src/Pure/type.ML Fri Jul 01 14:18:27 2005 +0200
+++ b/src/Pure/type.ML Fri Jul 01 14:19:36 2005 +0200
@@ -56,6 +56,7 @@
exception TUNIFY
val unify: tsig -> tyenv * int -> typ * typ -> tyenv * int
val raw_unify: typ * typ -> bool
+ val eq_type: tyenv -> typ * typ -> bool
(*extend and merge type signatures*)
val add_classes: Pretty.pp -> NameSpace.naming -> (bstring * class list) list -> tsig -> tsig
@@ -388,6 +389,13 @@
(unify empty_tsig (Vartab.empty, 0) (strip_sorts ty1, strip_sorts ty2); true)
handle TUNIFY => false;
+(*check whether two types are equal with respect to a type environment*)
+fun eq_type tye (T, T') =
+ (case (devar (T, tye), devar (T', tye)) of
+ (Type (s, Ts), Type (s', Ts')) =>
+ s = s' andalso ListPair.all (eq_type tye) (Ts, Ts')
+ | (U, U') => U = U');
+
(** extend and merge type signatures **)