src/Pure/pattern.ML
changeset 2751 673c4eefd2e1
parent 2725 9453616d4b80
child 2792 6c17c5ec3d8b
     1.1 --- a/src/Pure/pattern.ML	Fri Mar 07 10:22:54 1997 +0100
     1.2 +++ b/src/Pure/pattern.ML	Fri Mar 07 10:23:54 1997 +0100
     1.3 @@ -12,11 +12,14 @@
     1.4  TODO: optimize red by special-casing it
     1.5  *)
     1.6  
     1.7 +infix aeconv;
     1.8 +
     1.9  signature PATTERN =
    1.10    sig
    1.11    type type_sig
    1.12    type sg
    1.13    type env
    1.14 +  val aeconv            : term * term -> bool
    1.15    val eta_contract      : term -> term
    1.16    val eta_contract_atom : term -> term
    1.17    val match             : type_sig -> term * term
    1.18 @@ -289,16 +292,14 @@
    1.19  
    1.20  (*Tests whether 2 terms are alpha/eta-convertible and have same type.
    1.21    Note that Consts and Vars may have more than one type.*)
    1.22 -infix aeconv;
    1.23 -fun (Const(a,T)) aeconv (Const(b,U)) = a=b  andalso  T=U
    1.24 -  | (Free(a,T))  aeconv (Free(b,U))  = a=b  andalso  T=U
    1.25 -  | (Var(v,T))   aeconv (Var(w,U))   = v=w  andalso  T=U
    1.26 -  | (Bound i)    aeconv (Bound j)    = i=j
    1.27 -  | (Abs(_,T,t)) aeconv (Abs(_,U,u)) = (t aeconv u)  andalso  T=U
    1.28 -  | (Abs(_,T,t)) aeconv u            = t aeconv ((incr u)$Bound(0))
    1.29 -  | t            aeconv (Abs(_,U,u)) = ((incr t)$Bound(0)) aeconv u
    1.30 -  | (f$t)        aeconv (g$u)        = (f aeconv g)  andalso (t aeconv u)
    1.31 -  | _ aeconv _                       =  false;
    1.32 +fun t aeconv u = aconv_aux (eta_contract_atom t, eta_contract_atom u)
    1.33 +and aconv_aux (Const(a,T), Const(b,U)) = a=b  andalso  T=U
    1.34 +  | aconv_aux (Free(a,T),  Free(b,U))  = a=b  andalso  T=U
    1.35 +  | aconv_aux (Var(v,T),   Var(w,U))   = eq_ix(v,w) andalso  T=U
    1.36 +  | aconv_aux (Bound i,	   Bound j)    = i=j
    1.37 +  | aconv_aux (Abs(_,T,t), Abs(_,U,u)) = (t aeconv u)  andalso  T=U
    1.38 +  | aconv_aux (f$t,	   g$u)        = (f aeconv g)  andalso (t aeconv u)
    1.39 +  | aconv_aux _ =  false;
    1.40  
    1.41  
    1.42  fun match tsg (po as (pat,obj)) =