--- a/Nominal/Ex/SingleLet.thy	Thu Jun 24 19:32:33 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Thu Jun 24 21:35:11 2010 +0100
@@ -4,9 +4,9 @@
 
 atom_decl name
 
-declare [[STEPS = 14]]
+declare [[STEPS = 15]]
 
-nominal_datatype trm =
+nominal_datatype trm  =
   Var "name"
 | App "trm" "trm"
 | Lam x::"name" t::"trm"  bind_set x in t
@@ -21,6 +21,9 @@
 where
   "bn (As x y t) = {atom x}"
 
+typ trm
+typ assg
+
 thm trm_assg.fv
 thm trm_assg.supp
 thm trm_assg.eq_iff