--- a/Nominal/Ex/Ex2.thy	Tue May 25 00:24:41 2010 +0100
+++ b/Nominal/Ex/Ex2.thy	Wed May 26 15:34:54 2010 +0200
@@ -3,6 +3,7 @@
 begin
 
 text {* example 2 *}
+declare [[STEPS = 8]]
 
 atom_decl name
 
@@ -21,6 +22,13 @@
   "f PN = {}"
 | "f (PD x y) = {atom x, atom y}"
 | "f (PS x) = {atom x}"
+
+thm fv_trm_raw.simps[no_vars] fv_pat_raw.simps[no_vars] fv_f_raw.simps[no_vars] f_raw.simps[no_vars]
+thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars]
+
+
+
+
 thm trm_pat.bn
 thm trm_pat.perm
 thm trm_pat.induct