src/HOL/Analysis/metric_arith.ML

--- a/src/HOL/Analysis/metric_arith.ML	Thu Sep 09 16:53:40 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML	Thu Sep 09 17:20:41 2021 +0200
@@ -24,7 +24,7 @@
 fun IF_UNSOLVED' tac i = IF_UNSOLVED (tac i)
 fun REPEAT' tac i = REPEAT (tac i)
 
-fun free_in v ct = Cterms.defined (Misc_Legacy.cterm_frees ct) v
+fun free_in v ct = Cterms.defined (Cterms.build (Drule.add_frees_cterm ct)) v
 
 (* build a cterm set with elements cts of type ty *)
 fun mk_ct_set ctxt ty =