--- a/src/ZF/Coind/Values.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Coind/Values.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -67,7 +67,7 @@
 
 
 lemma v_constNE [simp]: "c \<in> Const \<Longrightarrow> v_const(c) \<noteq> 0"
-apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs)
+  unfolding QPair_def QInl_def QInr_def Val_ValEnv.con_defs
 apply (drule constNEE, auto)
 done