# HG changeset patch
# User paulson
# Date 857726666 -3600
# Node ID 74a9aead96c804303d907c32abe78b69c57f425e
# Parent  673c4eefd2e1372bbd11d46d57cf0d020fd5d391
Improved indentation of aconv

diff -r 673c4eefd2e1 -r 74a9aead96c8 src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Mar 07 10:23:54 1997 +0100
+++ b/src/Pure/term.ML	Fri Mar 07 10:24:26 1997 +0100
@@ -332,11 +332,11 @@
 (*Tests whether 2 terms are alpha-convertible and have same type.
   Note that constants and Vars may have more than one type.*)
 fun (Const(a,T)) aconv (Const(b,U)) = a=b  andalso  T=U
-  | (Free(a,T)) aconv (Free(b,U)) = a=b  andalso  T=U
-  | (Var(v,T)) aconv (Var(w,U)) =   eq_ix(v,w)  andalso  T=U
-  | (Bound i) aconv (Bound j)  =   i=j
+  | (Free(a,T))  aconv (Free(b,U))  = a=b  andalso  T=U
+  | (Var(v,T))   aconv (Var(w,U))   = eq_ix(v,w)  andalso  T=U
+  | (Bound i)    aconv (Bound j)    = i=j
   | (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u  andalso  T=U
-  | (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u)
+  | (f$t)        aconv (g$u)        = (f aconv g) andalso (t aconv u)
   | _ aconv _  =  false;
 
 (** Membership, insertion, union for terms **)