--- a/Nominal/Ex/Foo2.thy	Sun Dec 12 00:10:40 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Sun Dec 12 22:09:11 2010 +0000
@@ -24,6 +24,8 @@
  "bn (As x y t a) = [atom x] @ bn a"
 | "bn (As_Nil) = []"
 
+thm foo.exhaust
+
 ML {* 
   Variable.import;
   Variable.import true @{thms foo.exhaust} @{context}