diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Bali/Eval.thy	Wed Feb 12 08:37:06 2014 +0100
@@ -141,7 +141,7 @@
   where "\<lfloor>es\<rfloor>\<^sub>l == In3 es"
 
 definition undefined3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals" where
- "undefined3 = sum3_case (In1 \<circ> case_sum (\<lambda>x. undefined) (\<lambda>x. Unit))
+ "undefined3 = case_sum3 (In1 \<circ> case_sum (\<lambda>x. undefined) (\<lambda>x. Unit))
                      (\<lambda>x. In2 undefined) (\<lambda>x. In3 undefined)"
 
 lemma [simp]: "undefined3 (In1l x) = In1 undefined"