--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Aug 30 18:01:46 2025 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Aug 31 07:41:41 2025 +0200
@@ -1429,7 +1429,7 @@
|> fold_map (fn (name, result_thms) => (Global_Theory.add_thmss
[((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), [])]))
result_thms'
- |-> (fn notes => Code.declare_default_eqns_global (map (rpair true) (flat (flat (notes))))))
+ |-> (fn notes => Code.declare_default_eqns_global (map (rpair true) ((flat o flat) notes))))
in
thy'''
end