# HG changeset patch
# User haftmann
# Date 1444720874 -7200
# Node ID 9b6a0fb85fa3b65981cc190055dcf87045789641
# Parent  0dfcd0fb4172a7dd19a0e1dcdf53431f332c5cce
emphasized general nature of parameter

diff -r 0dfcd0fb4172 -r 9b6a0fb85fa3 src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/BNF_Def.thy	Tue Oct 13 09:21:14 2015 +0200
@@ -164,7 +164,7 @@
   by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2])
 
 lemma csquare_fstOp_sndOp:
-  "csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)"
+  "csquare (Collect (f (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)"
   unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp
 
 lemma snd_fst_flip: "snd xy = (fst \<circ> (%(x, y). (y, x))) xy"