src/FOL/FOL.thy

--- a/src/FOL/FOL.thy	Sun Sep 12 20:11:20 2021 +0200
+++ b/src/FOL/FOL.thy	Sun Sep 12 20:14:09 2021 +0200
@@ -203,7 +203,7 @@
   structure Blast = Blast
   (
     structure Classical = Cla
-    val Trueprop_const = dest_Const \<^const>\<open>Trueprop\<close>
+    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}