--- a/List_Prefix.thy	Sun Jun 23 03:55:49 2013 +0100
+++ b/List_Prefix.thy	Fri Sep 06 12:55:12 2013 +0100
@@ -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"