--- a/src/ZF/Coind/Values.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Coind/Values.thy Tue Sep 27 17:54:20 2022 +0100
@@ -101,7 +101,7 @@
done
lemma ve_empI: "ve_emp \<in> ValEnv"
-apply (unfold ve_emp_def)
+ unfolding ve_emp_def
apply (rule Val_ValEnv.intros)
apply (rule pmap_empI)
done