src/HOL/Library/Coinductive_List.thy

       with h h' MN have ?EqNIL by simp
       then show ?thesis ..
     next
       case (Some p)
       with h h' MN have "M = CONS (fst p) (h (snd p))"
-	and "N = CONS (fst p) (h' (snd p))"
+        and "N = CONS (fst p) (h' (snd p))"
         by (simp_all split: prod.split)
       then have ?EqCONS by (auto iff: Id_on_iff)
       then show ?thesis ..
     qed
   qed