# HG changeset patch
# User berghofe
# Date 1120220376 -7200
# Node ID bd4f7149ba1e01992a51eecba676e20ef85c6c7a
# Parent  d88271eb5b26c7d7b8b089fde743f4a9c02f0e98
Moved eq_type from envir.ML to type.ML

diff -r d88271eb5b26 -r bd4f7149ba1e src/Pure/type.ML
--- 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 **)