src/FOL/FOL.thy

 
 ML \<open>
   structure Blast = Blast
   (
     structure Classical = Cla
-    val Trueprop_const = dest_Const @{const Trueprop}
+    val Trueprop_const = dest_Const \<^const>\<open>Trueprop\<close>
     val equality_name = \<^const_name>\<open>eq\<close>
     val not_name = \<^const_name>\<open>Not\<close>
     val notE = @{thm notE}
     val ccontr = @{thm ccontr}
     val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac