--- a/src/FOL/FOL.thy Sat May 14 00:32:16 2011 +0200
+++ b/src/FOL/FOL.thy Sat May 14 11:42:43 2011 +0200
@@ -167,7 +167,7 @@
section {* Classical Reasoner *}
ML {*
-structure Cla = ClassicalFun
+structure Cla = Classical
(
val imp_elim = @{thm imp_elim}
val not_elim = @{thm notE}