diff -r 8d0294d877bd -r 107941e8fa01 src/HOL/Library/Pattern_Aliases.thy
--- a/src/HOL/Library/Pattern_Aliases.thy	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Library/Pattern_Aliases.thy	Tue Sep 28 22:14:44 2021 +0200
@@ -97,7 +97,7 @@
 
 fun check_pattern_syntax t =
   case strip_all t of
-    (vars, \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
+    (vars, \<^Const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
       let
         fun go (Const (\<^const_name>\<open>as\<close>, _) $ pat $ var, rhs) =
               let
@@ -126,7 +126,7 @@
 
 fun uncheck_pattern_syntax ctxt t =
   case strip_all t of
-    (vars, \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
+    (vars, \<^Const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
       let
         (* restricted to going down abstractions; ignores eta-contracted rhs *)
         fun go lhs (rhs as Const (\<^const_name>\<open>Let\<close>, _) $ pat $ Abs (name, typ, t)) ctxt frees =