src/HOL/Real_Asymp/exp_log_expression.ML

--- a/src/HOL/Real_Asymp/exp_log_expression.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Real_Asymp/exp_log_expression.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -164,8 +164,7 @@
         handle Pattern.MATCH => NONE
     fun rewrite_subterm prems ct (Abs (x, _, _)) =
       let
-        val (u, ctxt') = yield_singleton Variable.variant_fixes x ctxt;
-        val (v, ct') = Thm.dest_abs_name u ct;
+        val ((v, ct'), ctxt') = Variable.dest_abs_cterm ct ctxt;
         val (thm, prems) = rewrite' ctxt' prems (x :: bounds) thms ct'
       in
         if Thm.is_reflexive thm then