--- a/src/FOL/ex/Classical.thy Tue Oct 06 13:31:44 2015 +0200
+++ b/src/FOL/ex/Classical.thy Tue Oct 06 15:14:28 2015 +0200
@@ -363,7 +363,7 @@
text\<open>Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
fast DISCOVERS who killed Agatha.\<close>
-schematic_lemma "lives(agatha) & lives(butler) & lives(charles) &
+schematic_goal "lives(agatha) & lives(butler) & lives(charles) &
(killed(agatha,agatha) | killed(butler,agatha) | killed(charles,agatha)) &
(\<forall>x y. killed(x,y) --> hates(x,y) & ~richer(x,y)) &
(\<forall>x. hates(agatha,x) --> ~hates(charles,x)) &