--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Thu Oct 14 16:03:20 2021 +0200
@@ -308,7 +308,7 @@
if p t then t else
case Thm.term_of t of
_$_ => (find_cterm p (Thm.dest_fun t) handle CTERM _ => find_cterm p (Thm.dest_arg t))
- | Abs (_,_,_) => find_cterm p (Thm.dest_abs NONE t |> snd)
+ | Abs (_,_,_) => find_cterm p (Thm.dest_abs t |> snd)
| _ => raise CTERM ("find_cterm",[t]);
fun is_comb t = (case Thm.term_of t of _ $ _ => true | _ => false);
@@ -496,7 +496,7 @@
fun h (acc, t) =
case Thm.term_of t of
Const(\<^const_name>\<open>Ex\<close>,_)$Abs(_,_,_) =>
- h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+ h (Thm.dest_abs (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end
@@ -541,7 +541,7 @@
fun h (acc, t) =
case Thm.term_of t of
Const(\<^const_name>\<open>All\<close>,_)$Abs(_,_,_) =>
- h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+ h (Thm.dest_abs (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end