src/HOL/Analysis/metric_arith.ML

--- a/src/HOL/Analysis/metric_arith.ML	Thu Sep 09 14:05:31 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML	Thu Sep 09 14:50:26 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) (Misc_Legacy.cterm_frees ct) v
+fun free_in v ct = Cterms.defined (Misc_Legacy.cterm_frees ct) v
 
 (* build a cterm set with elements cts of type ty *)
 fun mk_ct_set ctxt ty =