--- a/List_Prefix.thy	Thu Jul 11 16:46:05 2013 +0100
+++ b/List_Prefix.thy	Thu Sep 12 10:34:11 2013 +0200
@@ -119,7 +119,7 @@
   by (auto simp add: prefix_def)
 
 lemma prefix_same_cases:
-  "(xs\<^isub>1::'a list) \<le> ys \<Longrightarrow> xs\<^isub>2 \<le> ys \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1"
+  "(xs\<^sub>1::'a list) \<le> ys \<Longrightarrow> xs\<^sub>2 \<le> ys \<Longrightarrow> xs\<^sub>1 \<le> xs\<^sub>2 \<or> xs\<^sub>2 \<le> xs\<^sub>1"
   unfolding prefix_def by (metis append_eq_append_conv2)
 
 lemma set_mono_prefix: "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"