1.1 --- a/src/HOL/Imperative_HOL/ex/Sublist.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -490,7 +490,6 @@
     1.4    moreover
     1.5    from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
     1.6      by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
     1.7 -  moreover
     1.8    ultimately show ?thesis by (simp add: multiset_of_append)
     1.9  qed
    1.10