--- a/Nominal/Ex/Ex4.thy	Mon May 17 12:46:51 2010 +0100
+++ b/Nominal/Ex/Ex4.thy	Mon May 17 16:29:33 2010 +0200
@@ -2,8 +2,7 @@
 imports "../NewParser"
 begin
 
-declare [[STEPS = 4]]
-(* alpha does not work for this type *)
+declare [[STEPS = 5]]
 
 atom_decl name
 
@@ -28,8 +27,9 @@
 thm permute_trm_raw_permute_pat_raw.simps
 thm fv_trm_raw.simps fv_pat_raw.simps fv_f_raw.simps
 
-(* thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars]*)
+thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars]
 
+(*
 inductive 
  alpha_trm_raw and alpha_pat_raw and alpha_f_raw
 where
@@ -60,6 +60,7 @@
 | "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>
   \<Longrightarrow> alpha_f_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)"
+*)
 
 lemmas all = alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros
 
@@ -78,7 +79,7 @@
 apply(rule all)
 done
 
- 
+
 
 end