# HG changeset patch
# User wenzelm
# Date 1631470449 -7200
# Node ID 33f13d2d211c3f6c775c06ae347dee08cac1854a
# Parent  16e5870fe21eb6f7e87646fd1571c4a2209583ac
clarified antiquotations;

diff -r 16e5870fe21e -r 33f13d2d211c 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}