--- a/src/HOL/Codatatype/Examples/TreeFsetI.thy Fri Sep 14 12:09:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy Fri Sep 14 12:09:27 2012 +0200
@@ -52,7 +52,7 @@
lemmas treeFsetI_coind = mp[OF treeFsetI.pred_coinduct]
lemma "tmap (f o g) x = tmap f (tmap g x)"
-by (intro treeFsetI_coind[where phi="%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])
+by (intro treeFsetI_coind[where P="%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])
force+
end