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