--- a/Nominal/Ex/Foo1.thy	Mon Nov 15 09:52:29 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Mon Nov 15 20:54:01 2010 +0000
@@ -218,6 +218,9 @@
 apply(simp add: Abs_fresh_star)
 done
 
+thm strong_exhaust1 foo.exhaust(1)
+
+
 
 lemma strong_exhaust2:
   assumes "\<And>x y t. as = As x y t \<Longrightarrow> P"