clarified signature -- avoid clones;

--- a/src/HOL/Tools/BNF/bnf_comp.ML	Sun Oct 24 22:10:28 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Oct 25 11:41:03 2021 +0200
@@ -153,15 +153,10 @@
   "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
 
 
-(*copied from Envir.expand_term_free*)
-fun expand_term_const defs =
-  let
-    val eqs = map ((fn ((x, U), u) => (x, (U, u))) o apfst dest_Const) defs;
-    val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
-  in Envir.expand_term get end;
-
 val id_bnf_def = @{thm id_bnf_def};
-val expand_id_bnf_def = expand_term_const [Thm.prop_of id_bnf_def |> Logic.dest_equals];
+val expand_id_bnf_def =
+  Envir.expand_term_defs dest_Const
+    [Thm.prop_of id_bnf_def |> Logic.dest_equals |> apfst dest_Const];
 
 fun is_sum_prod_natLeq (Const (\<^const_name>\<open>csum\<close>, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
   | is_sum_prod_natLeq (Const (\<^const_name>\<open>cprod\<close>, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sun Oct 24 22:10:28 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Oct 25 11:41:03 2021 +0200
@@ -65,7 +65,7 @@
           val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
           val pre_rhs =
             fold (curry HOLogic.mk_conj) (map HOLogic.dest_Trueprop prems'') inner_t
-          val rhs = Envir.expand_term_frees subst pre_rhs
+          val rhs = Envir.expand_term_defs dest_Free subst pre_rhs
         in
           (case try_destruct_case thy (var_names @ names') rhs of
             NONE => [(subst, rhs)]
@@ -116,7 +116,7 @@
               val constT = map fastype_of frees ---> HOLogic.boolT
               val lhs = list_comb (Const (full_constname, constT), frees)
               fun mk_def (subst, rhs) =
-                Logic.mk_equals (fold Envir.expand_term_frees (map single subst) lhs, rhs)
+                Logic.mk_equals (fold (Envir.expand_term_defs dest_Free) (map single subst) lhs, rhs)
               val new_defs = map mk_def srs
               val (definition, thy') = thy
               |> Sign.add_consts [(Binding.name constname, constT, NoSyn)]

--- a/src/Pure/Isar/local_defs.ML	Sun Oct 24 22:10:28 2021 +0200
+++ b/src/Pure/Isar/local_defs.ML	Mon Oct 25 11:41:03 2021 +0200
@@ -93,7 +93,7 @@
       (Names.empty, Names.build (fold (Names.add_set o #1 o head_of_def o Thm.term_of) defs))
   #> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
 
-val expand_term = Envir.expand_term_frees o map (abs_def o Thm.term_of);
+val expand_term = Envir.expand_term_defs dest_Free o map (abs_def o Thm.term_of);
 
 fun def_export _ defs = (expand defs, expand_term defs);
 
@@ -125,7 +125,7 @@
       |> Proof_Context.add_fixes [(x, SOME T, mx)];
     val lhs = Free (x', T);
     val _ = cert_def ctxt' (K []) (Logic.mk_equals (lhs, rhs));
-    fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]);
+    fun abbrev_export _ _ = (I, Envir.expand_term_defs dest_Free [((x', T), rhs)]);
     val (_, ctxt'') = Assumption.add_assms abbrev_export [] ctxt';
   in ((lhs, rhs), ctxt'') end;
 

--- a/src/Pure/envir.ML	Sun Oct 24 22:10:28 2021 +0200
+++ b/src/Pure/envir.ML	Mon Oct 25 11:41:03 2021 +0200
@@ -48,7 +48,7 @@
   val subst_term: Type.tyenv * tenv -> term -> term
   val expand_atom: typ -> typ * term -> term
   val expand_term: (term -> (typ * term) option) -> term -> term
-  val expand_term_frees: ((string * typ) * term) list -> term -> term
+  val expand_term_defs: (term -> string * typ) -> ((string * typ) * term) list -> term -> term
 end;
 
 structure Envir: ENVIR =
@@ -415,10 +415,10 @@
       end;
   in expand end;
 
-fun expand_term_frees defs =
+fun expand_term_defs dest defs =
   let
-    val eqs = map (fn ((x, U), u) => (x, (U, u))) defs;
-    val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE;
+    val eqs = map (fn ((x, U), u) => (x: string, (U, u))) defs;
+    fun get t = (case try dest t of SOME (x, _: typ) => AList.lookup (op =) eqs x | _ => NONE);
   in expand_term get end;
 
 end;