diff -r 118a0ca16381 -r 387fcbd33820 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Tue Jun 01 15:46:07 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Wed Jun 02 11:37:51 2010 +0200
@@ -4,9 +4,6 @@
 
 atom_decl name
 
-ML {*  Function.add_function *}
-
-ML {* print_depth 50 *}
 declare [[STEPS = 9]]
 
 
@@ -18,11 +15,11 @@
 | Foo x::"name" y::"name" t::"trm" bind_set x in y t
 | Bar x::"name" y::"name" t::"trm" bind y x in t x y
 and assg =
-  As "name" "trm"
+  As "name" "name" "trm" "name"
 binder
   bn::"assg \<Rightarrow> atom set"
 where
-  "bn (As x t) = {atom x}"
+  "bn (As x y t z) = {atom x}"
 
 ML {* Inductive.the_inductive *}
 thm trm_assg.fv