--- a/Nominal/Ex/Foo2.thy	Tue Dec 07 19:16:09 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Wed Dec 08 12:37:25 2010 +0000
@@ -30,6 +30,7 @@
 thm foo.perm_bn_simps
 thm foo.bn_finite
 
+
 thm foo.distinct
 thm foo.induct
 thm foo.inducts
@@ -45,12 +46,9 @@
 thm foo.supp
 thm foo.fresh
 
-text {*
-  tests by cu
-*}
 
 
-text {* *}
+
 
 
 (*
@@ -71,6 +69,25 @@
 sorry 
 *)
 
+thm foo.exhaust
+
+ML {*
+fun strip_prems_concl trm =
+  (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm)
+*}
+
+
+ML {*
+  @{thms foo.exhaust}
+  |> map prop_of
+  |> map strip_prems_concl
+  |> map fst
+  |> map (map (Syntax.string_of_term @{context}))
+  |> map cat_lines
+  |> cat_lines
+  |> writeln 
+*}
+
 lemma test6:
   fixes c::"'a::fs"
   assumes "\<exists>name. y = Var name \<Longrightarrow> P"