# HG changeset patch
# User paulson
# Date 857726634 -3600
# Node ID 673c4eefd2e1372bbd11d46d57cf0d020fd5d391
# Parent  fe3799355b5e56b02eb7a124f8c8dc0082011cd1
Corrected aeconv and exported it

diff -r fe3799355b5e -r 673c4eefd2e1 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri Mar 07 10:22:54 1997 +0100
+++ b/src/Pure/pattern.ML	Fri Mar 07 10:23:54 1997 +0100
@@ -12,11 +12,14 @@
 TODO: optimize red by special-casing it
 *)
 
+infix aeconv;
+
 signature PATTERN =
   sig
   type type_sig
   type sg
   type env
+  val aeconv            : term * term -> bool
   val eta_contract      : term -> term
   val eta_contract_atom : term -> term
   val match             : type_sig -> term * term
@@ -289,16 +292,14 @@
 
 (*Tests whether 2 terms are alpha/eta-convertible and have same type.
   Note that Consts and Vars may have more than one type.*)
-infix aeconv;
-fun (Const(a,T)) aeconv (Const(b,U)) = a=b  andalso  T=U
-  | (Free(a,T))  aeconv (Free(b,U))  = a=b  andalso  T=U
-  | (Var(v,T))   aeconv (Var(w,U))   = v=w  andalso  T=U
-  | (Bound i)    aeconv (Bound j)    = i=j
-  | (Abs(_,T,t)) aeconv (Abs(_,U,u)) = (t aeconv u)  andalso  T=U
-  | (Abs(_,T,t)) aeconv u            = t aeconv ((incr u)$Bound(0))
-  | t            aeconv (Abs(_,U,u)) = ((incr t)$Bound(0)) aeconv u
-  | (f$t)        aeconv (g$u)        = (f aeconv g)  andalso (t aeconv u)
-  | _ aeconv _                       =  false;
+fun t aeconv u = aconv_aux (eta_contract_atom t, eta_contract_atom u)
+and aconv_aux (Const(a,T), Const(b,U)) = a=b  andalso  T=U
+  | aconv_aux (Free(a,T),  Free(b,U))  = a=b  andalso  T=U
+  | aconv_aux (Var(v,T),   Var(w,U))   = eq_ix(v,w) andalso  T=U
+  | aconv_aux (Bound i,	   Bound j)    = i=j
+  | aconv_aux (Abs(_,T,t), Abs(_,U,u)) = (t aeconv u)  andalso  T=U
+  | aconv_aux (f$t,	   g$u)        = (f aeconv g)  andalso (t aeconv u)
+  | aconv_aux _ =  false;
 
 
 fun match tsg (po as (pat,obj)) =