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