src/HOL/Tools/Qelim/qelim.ML

--- a/src/HOL/Tools/Qelim/qelim.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -32,7 +32,7 @@
   | Const(\<^const_name>\<open>Ex\<close>,_)$Abs(s,_,_) =>
     let
      val (e,p0) = Thm.dest_comb p
-     val (x,p') = Thm.dest_abs (SOME s) p0
+     val (x,p') = Thm.dest_abs_name s p0
      val env' = ins x env
      val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p')
                    |> Drule.arg_cong_rule e