--- a/Nominal/Ex/Term8.thy	Mon May 17 16:29:33 2010 +0200
+++ b/Nominal/Ex/Term8.thy	Mon May 17 17:31:18 2010 +0200
@@ -6,9 +6,7 @@
 
 atom_decl name
 
-(* this should work but gives an error at the moment:
-   in alpha_bn_rsp proof.
-*)
+ML {* val _ = cheat_alpha_bn_rsp := true *}
 
 nominal_datatype foo =
   Foo0 "name"
@@ -22,6 +20,7 @@
   "bv (Bar0 x) = {}"
 | "bv (Bar1 v x b) = {atom v}"
 
+thm foo_bar.supp
 
 end