src/FOL/FOL.thy

--- a/src/FOL/FOL.thy	Sat May 14 13:26:55 2011 +0200
+++ b/src/FOL/FOL.thy	Sat May 14 13:32:33 2011 +0200
@@ -201,7 +201,7 @@
   structure Blast = Blast
   (
     structure Classical = Cla
-    val thy = @{theory}
+    val Trueprop_const = dest_Const @{const Trueprop}
     val equality_name = @{const_name eq}
     val not_name = @{const_name Not}
     val notE = @{thm notE}