src/FOL/FOL.thy

 
 ML {*
   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}
     val ccontr = @{thm ccontr}
     val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac