--- a/Nominal/Ex/Foo2.thy Wed Dec 08 13:05:04 2010 +0000 +++ b/Nominal/Ex/Foo2.thy Wed Dec 08 13:16:25 2010 +0000 @@ -76,7 +76,6 @@ (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm) *} - ML {* @{thms foo.exhaust} |> map prop_of