--- a/Nominal/Ex/Lambda.thy	Sat Aug 21 16:20:10 2010 +0800
+++ b/Nominal/Ex/Lambda.thy	Sat Aug 21 17:55:42 2010 +0800
@@ -3,12 +3,14 @@
 begin
 
 atom_decl name
-declare [[STEPS = 20]]
+declare [[STEPS = 2]]
 
-nominal_datatype  lam =
+nominal_datatype 'a lam =
   Var "name"
-| App "lam" "lam"
-| Lam x::"name" l::"lam"  bind x in l
+| App "'a lam" "'a lam"
+| Lam x::"name" l::"'a lam"  bind x in l
+
+ML {* Datatype.read_typ *}
 
 
 thm eq_iff