# HG changeset patch
# User wenzelm
# Date 1633364356 -7200
# Node ID 2fdf37577f7b1fce6dd3fe0771e2cb98133a28c8
# Parent  63a697f1fb8f6b25a4fd2e9d5e99dfca2424ae09
tuned;

diff -r 63a697f1fb8f -r 2fdf37577f7b src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Oct 04 18:12:55 2021 +0200
+++ b/src/Pure/term.ML	Mon Oct 04 18:19:16 2021 +0200
@@ -165,6 +165,7 @@
   val could_beta_contract: term -> bool
   val could_eta_contract: term -> bool
   val could_beta_eta_contract: term -> bool
+  val used_free: string -> term -> bool
   val dest_abs: string * typ * term -> string * term
   val dummy_pattern: typ -> term
   val dummy: term
diff -r 63a697f1fb8f -r 2fdf37577f7b src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Oct 04 18:12:55 2021 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Oct 04 18:19:16 2021 +0200
@@ -623,8 +623,7 @@
   | translate_term ctxt algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
       let
         val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize (SOME false) v, ty, t);
-        val v'' = if member (op =) (Term.add_free_names t' []) v'
-          then SOME v' else NONE
+        val v'' = if Term.used_free v' t' then SOME v' else NONE
       in
         translate_typ ctxt algbr eqngr permissive ty
         ##>> translate_term ctxt algbr eqngr permissive some_thm (t', some_abs)