--- a/src/HOL/BNF_GFP.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/BNF_GFP.thy Wed Feb 12 08:35:57 2014 +0100
@@ -27,13 +27,13 @@
lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
by fast
-lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
+lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
by (auto split: sum.splits)
-lemma sum_case_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> sum_case g h = f"
+lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
apply rule
apply (rule ext, force split: sum.split)
-by (rule ext, metis sum_case_o_inj(2))
+by (rule ext, metis case_sum_o_inj(2))
lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
by fast