diff -r a8e96847523c -r eab03e9cee8a src/HOL/Import/HOL_Light_Maps.thy
--- a/src/HOL/Import/HOL_Light_Maps.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -210,7 +210,7 @@
 
 lemma sum_RECURSION:
   "\<forall>Inl' Inr'. \<exists>fn. (\<forall>a :: 'A. fn (Inl a) = (Inl' a :: 'Z)) \<and> (\<forall>a :: 'B. fn (Inr a) = Inr' a)"
-  by (intro allI, rule_tac x="sum_case Inl' Inr'" in exI) auto
+  by (intro allI, rule_tac x="case_sum Inl' Inr'" in exI) auto
 
 lemma OUTL[import_const "OUTL" : "Sum_Type.projl"]:
   "Sum_Type.projl (Inl x) = x"