--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Mon Sep 06 13:49:36 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Mon Sep 06 14:05:22 2021 +0200
@@ -868,10 +868,10 @@
then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm)
else raise Failure "substitutable_monomial"
| \<^term>\<open>(+) :: real \<Rightarrow> _\<close>$_$_ =>
- (substitutable_monomial (merge (op aconvc) (fvs, Drule.cterm_frees_of (Thm.dest_arg tm)))
+ (substitutable_monomial (merge (op aconvc) (fvs, Misc_Legacy.cterm_frees (Thm.dest_arg tm)))
(Thm.dest_arg1 tm)
handle Failure _ =>
- substitutable_monomial (merge (op aconvc) (fvs, Drule.cterm_frees_of (Thm.dest_arg1 tm)))
+ substitutable_monomial (merge (op aconvc) (fvs, Misc_Legacy.cterm_frees (Thm.dest_arg1 tm)))
(Thm.dest_arg tm))
| _ => raise Failure "substitutable_monomial")