changeset 74518 | de4f151c2a34 |
parent 74113 | 228adc502803 |
child 74525 | c960bfcb91db |
--- a/src/HOL/Real_Asymp/exp_log_expression.ML Thu Oct 14 15:24:28 2021 +0200 +++ b/src/HOL/Real_Asymp/exp_log_expression.ML Thu Oct 14 16:03:20 2021 +0200 @@ -165,7 +165,7 @@ fun rewrite_subterm prems ct (Abs (x, _, _)) = let val (u, ctxt') = yield_singleton Variable.variant_fixes x ctxt; - val (v, ct') = Thm.dest_abs (SOME u) ct; + val (v, ct') = Thm.dest_abs_name u ct; val (thm, prems) = rewrite' ctxt' prems (x :: bounds) thms ct' in if Thm.is_reflexive thm then