1.1 --- a/src/ZF/ex/LList.thy	Wed Jul 02 17:34:45 2014 +0200
     1.2 +++ b/src/ZF/ex/LList.thy	Wed Jun 11 14:24:23 2014 +1000
     1.3 @@ -173,7 +173,7 @@
     1.4  apply (rule_tac X = "{<l,l>. l \<in> llist (A) }" in lleq.coinduct)
     1.5  apply blast
     1.6  apply safe
     1.7 -apply (erule_tac a=l in llist.cases, fast+)
     1.8 +apply (erule_tac a=la in llist.cases, fast+)
     1.9  done
    1.10  
    1.11