--- a/Nominal/Ex/Test.thy	Sun May 16 12:41:27 2010 +0100
+++ b/Nominal/Ex/Test.thy	Mon May 17 12:00:54 2010 +0100
@@ -5,6 +5,8 @@
 (* This file contains only the examples that are not supposed to work yet. *)
 
 
+declare [[STEPS = 2]]
+
 atom_decl name
 
 (* example 4 from Terms.thy *)
@@ -12,12 +14,11 @@
    defined fv and defined alpha... *)
 (* lists-datastructure does not work yet *)
 
-(*
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm list"
 | Lm x::"name" t::"trm"  bind x in t
-*)
+
 
 (*
 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]