--- a/src/HOL/Library/RBT.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Library/RBT.thy Wed Feb 12 08:35:57 2014 +0100
@@ -135,7 +135,7 @@
by transfer (rule rbt_lookup_map)
lemma fold_fold:
- "fold f t = List.fold (prod_case f) (entries t)"
+ "fold f t = List.fold (case_prod f) (entries t)"
by transfer (rule RBT_Impl.fold_def)
lemma impl_of_empty:
@@ -175,7 +175,7 @@
by transfer (simp add: keys_entries)
lemma fold_def_alt:
- "fold f t = List.fold (prod_case f) (entries t)"
+ "fold f t = List.fold (case_prod f) (entries t)"
by transfer (auto simp: RBT_Impl.fold_def)
lemma distinct_entries: "distinct (List.map fst (entries t))"