1.1 --- a/src/HOL/Codatatype/Examples/Misc_Data.thy	Wed Sep 05 15:40:29 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Examples/Misc_Data.thy	Wed Sep 05 15:53:31 2012 +0200
     1.3 @@ -102,6 +102,7 @@
     1.4   and fail2 = F2 "fail1 fset" fail1
     1.5  *)
     1.6  
     1.7 +(* SLOW
     1.8  data ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
     1.9   and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"
    1.10   and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5"
    1.11 @@ -120,6 +121,7 @@
    1.12       and ('a, 'c) D6' = A6' "('a, 'c) D7'"
    1.13       and ('a, 'c) D7' = A7' "('a, 'c) D8'"
    1.14       and ('a, 'c) D8' = A8' "('a, 'c) D1' list"
    1.15 +*)
    1.16  
    1.17  (* fail:
    1.18  data tt1 = TT11 tt2 tt3 | TT12 tt2 tt4
    1.19 @@ -138,6 +140,7 @@
    1.20   and tt3 = TT3 tt1
    1.21   and tt4 = TT4
    1.22  
    1.23 +(* SLOW
    1.24  data s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2
    1.25   and s2 = S21 s7 s5 | S22 s5 s4 s6
    1.26   and s3 = S31 s1 s7 s2 | S32 s3 s3 | S33 s4 s5
    1.27 @@ -146,5 +149,6 @@
    1.28   and s6 = S61 s6 | S62 s1 s2 | S63 s6
    1.29   and s7 = S71 s8 | S72 s5
    1.30   and s8 = S8 nat
    1.31 +*)
    1.32  
    1.33  end