--- a/src/ZF/Constructible/AC_in_L.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy Tue Sep 27 17:54:20 2022 +0100
@@ -216,7 +216,7 @@
text\<open>Not needed--but interesting?\<close>
theorem formula_lepoll_nat: "formula \<lesssim> nat"
apply (insert nat_times_nat_lepoll_nat)
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (blast intro: Nat_Times_Nat.inj_formula_nat Nat_Times_Nat.intro)
done
@@ -447,7 +447,7 @@
lemma well_ord_L_r:
"Ord(i) \<Longrightarrow> \<exists>r. well_ord(Lset(i), r)"
apply (insert nat_times_nat_lepoll_nat)
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (blast intro: Nat_Times_Nat.well_ord_L_r Nat_Times_Nat.intro)
done