--- 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;