--- 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
--- 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)