1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Sep 18 15:33:30 2013 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Sep 18 15:33:31 2013 +0200
     1.3 @@ -1721,7 +1721,7 @@
     1.4      primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
     1.5        "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lnull (lappend xs ys)" |
     1.6        "lhd (lappend xs ys) = lhd (if lnull xs then ys else xs)" |
     1.7 -      "ltl (lappend xs ys) = ltl (if lnull xs then ys else xs)"
     1.8 +      "ltl (lappend xs ys) = (if xs = LNil then ltl ys else lappend (ltl xs) ys)"
     1.9      .
    1.10  (*<*)
    1.11      end