src/HOL/BNF/BNF_Def.thy

--- a/src/HOL/BNF/BNF_Def.thy	Wed May 08 09:45:30 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy	Wed May 08 11:57:42 2013 +0200
@@ -182,7 +182,7 @@
   A \<subseteq> Collect (split Q)"
   by fastforce
 
-lemma predicate2_cong: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
+lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
 by metis
 
 ML_file "Tools/bnf_def_tactics.ML"