src/HOL/Analysis/metric_arith.ML

--- a/src/HOL/Analysis/metric_arith.ML	Mon Sep 06 13:49:36 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML	Mon Sep 06 14:05:22 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 = member (op aconvc) (Drule.cterm_frees_of ct) v
+fun free_in v ct = member (op aconvc) (Misc_Legacy.cterm_frees ct) v
 
 (* build a cterm set with elements cts of type ty *)
 fun mk_ct_set ctxt ty =