diff -r c434f4e74947 -r de4f151c2a34 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -145,7 +145,7 @@
 
 fun get_pmi_term t =
   let val (x,eq) =
-     (Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg)
+     (Thm.dest_abs o Thm.dest_arg o snd o Thm.dest_abs o Thm.dest_arg)
         (Thm.dest_arg t)
 in (Thm.lambda x o Thm.dest_arg o Thm.dest_arg) eq end;
 
@@ -348,7 +348,7 @@
 
 fun unify ctxt q =
  let
-  val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE
+  val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs
   val x = Thm.term_of cx
   val ins = insert (op = : int * int -> bool)
   fun h (acc,dacc) t =
@@ -436,8 +436,8 @@
 val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1;
 val [A_v,B_v] =
   map (fn th => Thm.cprop_of th |> funpow 2 Thm.dest_arg
-    |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
-    |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg
+    |> Thm.dest_abs |> snd |> Thm.dest_arg1 |> Thm.dest_arg
+    |> Thm.dest_abs |> snd |> Thm.dest_fun |> Thm.dest_arg
     |> Thm.term_of |> dest_Var) [asetP, bsetP];
 
 val D_v = (("D", 0), \<^typ>\<open>int\<close>);
@@ -446,7 +446,7 @@
 let
 
  val uth = unify ctxt q
- val (x,p) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of uth))
+ val (x,p) = Thm.dest_abs (Thm.dest_arg (Thm.rhs_of uth))
  val ins = insert (op aconvc)
  fun h t (bacc,aacc,dacc) =
   case (whatis x t) of
@@ -717,7 +717,7 @@
 fun strip_objall ct =
  case Thm.term_of ct of
   Const (\<^const_name>\<open>All\<close>, _) $ Abs (xn,_,_) =>
-   let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
+   let val (a,(v,t')) = (apsnd (Thm.dest_abs_name xn) o Thm.dest_comb) ct
    in apfst (cons (a,v)) (strip_objall t')
    end
 | _ => ([],ct);
@@ -798,7 +798,7 @@
   fun h acc t = if ty cts t then insert (op aconvc) t acc else
    case Thm.term_of t of
     _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
-  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
+  | Abs(_,_,_) => Thm.dest_abs t ||> h acc |> uncurry (remove (op aconvc))
   | _ => acc
  in h [] ct end
 end;