diff -r 1466f8a2f6dd -r 28a582aa25dd src/HOL/HOLCF/Pcpo.thy --- a/src/HOL/HOLCF/Pcpo.thy Sun Sep 12 20:52:39 2021 +0200 +++ b/src/HOL/HOLCF/Pcpo.thy Sun Sep 12 22:31:51 2021 +0200 @@ -156,7 +156,7 @@ translations "UU" \ "CONST bottom" text \Simproc to rewrite \<^term>\\ = x\ to \<^term>\x = \\.\ -setup \Reorient_Proc.add (fn Const(\<^const_name>\bottom\, _) => true | _ => false)\ +setup \Reorient_Proc.add (fn \<^Const_>\bottom _\ => true | _ => false)\ simproc_setup reorient_bottom ("\ = x") = Reorient_Proc.proc text \useful lemmas about \<^term>\\\\