--- a/src/HOL/Library/Pattern_Aliases.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Library/Pattern_Aliases.thy Sat Jan 05 17:24:33 2019 +0100
@@ -97,7 +97,7 @@
fun check_pattern_syntax t =
case strip_all t of
- (vars, @{const Trueprop} $ (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 Trueprop} $ (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 =