src/ZF/ex/LList.thy

 lemma equal_llist_implies_leq:
      "[| l=l';  l \<in> llist(A) |] ==> <l,l'> \<in> lleq(A)"
 apply (rule_tac X = "{<l,l>. l \<in> llist (A) }" in lleq.coinduct)
 apply blast
 apply safe
-apply (erule_tac a=l in llist.cases, fast+)
+apply (erule_tac a=la in llist.cases, fast+)
 done
 
 
 (*** Lazy List Functions ***)