diff -r 029f8aabed12 -r 5dc48e1af733 Nominal/Ex/Test.thy
--- a/Nominal/Ex/Test.thy	Tue May 18 14:40:05 2010 +0100
+++ b/Nominal/Ex/Test.thy	Wed May 19 12:43:38 2010 +0100
@@ -2,12 +2,22 @@
 imports "../NewParser"
 begin
 
+declare [[STEPS = 4]]
+
+atom_decl name
+
+(*
+nominal_datatype trm =
+  Vr "name"
+| Ap "trm" "trm"
+
+thm fv_trm_raw.simps[no_vars]
+*)
 (* This file contains only the examples that are not supposed to work yet. *)
 
 
 declare [[STEPS = 2]]
 
-atom_decl name
 
 (* example 4 from Terms.thy *)
 (* fv_eqvt does not work, we need to repaire defined permute functions