
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" \<rightharpoonup> "CONST bottom"
 
 text \<open>Simproc to rewrite \<^term>\<open>\<bottom> = x\<close> to \<^term>\<open>x = \<bottom>\<close>.\<close>
-setup \<open>Reorient_Proc.add (fn Const(\<^const_name>\<open>bottom\<close>, _) => true | _ => false)\<close>
+setup \<open>Reorient_Proc.add (fn \<^Const_>\<open>bottom _\<close> => true | _ => false)\<close>
 simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
 
 text \<open>useful lemmas about \<^term>\<open>\<bottom>\<close>\<close>




