--- a/src/HOL/Real_Asymp/real_asymp.ML	Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Real_Asymp/real_asymp.ML	Sun Aug 04 17:39:47 2024 +0200
@@ -53,7 +53,7 @@
 fun prove_landau ectxt l f g =
   let
     val ctxt = get_ctxt ectxt
-    val l' = l |> dest_Const |> fst
+    val l' = dest_Const_name l
     val basis = Asymptotic_Basis.default_basis
     val ([thm1, thm2], basis) = Exp.expand_terms ectxt [f, g] basis
     val prover =