--- a/Nominal/Ex/Term8.thy	Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/Term8.thy	Thu Aug 26 02:08:00 2010 +0800
@@ -6,21 +6,21 @@
 
 atom_decl name
 
-ML {* val _ = cheat_alpha_bn_rsp := true *}
-
 nominal_datatype foo =
   Foo0 "name"
-| Foo1 b::"bar" f::"foo" bind_set "bv b" in f
+| Foo1 b::"bar" f::"foo" bind (set) "bv b" in f
 and bar =
   Bar0 "name"
-| Bar1 "name" s::"name" b::"bar" bind_set s in b
+| Bar1 "name" s::"name" b::"bar" bind (set) s in b
 binder
   bv
 where
   "bv (Bar0 x) = {}"
 | "bv (Bar1 v x b) = {atom v}"
 
+(*
 thm foo_bar.supp
+*)
 
 end