--- a/src/HOL/HOLCF/Cpodef.thy	Thu Dec 12 16:57:06 2024 +0100
+++ b/src/HOL/HOLCF/Cpodef.thy	Thu Dec 12 17:07:09 2024 +0100
@@ -24,9 +24,9 @@
   apply (rule class.po.intro)
   apply (unfold below)
     apply (rule below_refl)
-   apply (erule (1) below_trans)
+   apply (fact below_trans)
   apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
-  apply (erule (1) below_antisym)
+  apply (fact below_antisym)
   done
 
 lemmas typedef_po_class = below.typedef_class_po [THEN po.intro_of_class]