diff -r 92db671e0ac6 -r 415354b68f0c src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Fri Sep 06 10:56:40 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Fri Sep 06 10:56:40 2013 +0200
@@ -55,7 +55,7 @@
 
 lift_definition  is_empty_ivl :: "ivl \<Rightarrow> bool" is is_empty_rep
 apply(auto simp: eq_ivl_def \<gamma>_rep_cases is_empty_rep_def)
-apply(auto simp: not_less less_eq_extended_cases split: extended.splits)
+apply(auto simp: not_less less_eq_extended_case split: extended.splits)
 done
 
 lemma eq_ivl_iff: "eq_ivl p1 p2 = (is_empty_rep p1 & is_empty_rep p2 | p1 = p2)"