src/HOL/Imperative_HOL/ex/Sublist.thy

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