# HG changeset patch
# User wenzelm
# Date 1638799815 -3600
# Node ID fa5476c547315c6d0230c224faf30530228448bc
# Parent  2df334453c4cfbfdfdf2ca63f139786dd6291357
tuned proof;

diff -r 2df334453c4c -r fa5476c54731 src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Mon Dec 06 12:39:59 2021 +0100
+++ b/src/HOL/BNF_Def.thy	Mon Dec 06 15:10:15 2021 +0100
@@ -139,7 +139,7 @@
 
 lemma pick_middlep:
   "(P OO Q) a c \<Longrightarrow> P a (pick_middlep P Q a c) \<and> Q (pick_middlep P Q a c) c"
-  unfolding pick_middlep_def apply(rule someI_ex) by auto
+  unfolding pick_middlep_def by (rule someI_ex) auto
 
 definition fstOp where
   "fstOp P Q ac = (fst ac, pick_middlep P Q (fst ac) (snd ac))"