diff -r f38adea0591c -r 5111dadd1162 Nominal/Ex/Ex4.thy
--- a/Nominal/Ex/Ex4.thy	Thu May 13 18:19:48 2010 +0100
+++ b/Nominal/Ex/Ex4.thy	Thu May 13 19:06:54 2010 +0100
@@ -49,11 +49,13 @@
    alpha_f_raw pat_raw pat_rawa\<rbrakk>
    \<Longrightarrow> alpha_trm_raw (Foo2_raw name pat_raw trm_raw) (Foo2_raw namea pat_rawa trm_rawa)"
 
+(* alpha_pat_raw *)
 | "alpha_pat_raw PN_raw PN_raw"
 | "name = namea \<Longrightarrow> alpha_pat_raw (PS_raw name) (PS_raw namea)"
 | "\<lbrakk>alpha_pat_raw pat_raw1 pat_raw1a; alpha_pat_raw pat_raw2 pat_raw2a\<rbrakk>
    \<Longrightarrow> alpha_pat_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)"
 
+(* alpha_f_raw *)
 | "alpha_f_raw PN_raw PN_raw"
 | "alpha_f_raw (PS_raw name) (PS_raw namea)"
 | "\<lbrakk>alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\<rbrakk>