src/HOL/HOL.thy

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