1.1 --- a/src/HOL/Lazy_Sequence.thy	Thu Oct 20 08:20:35 2011 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Thu Oct 20 09:11:13 2011 +0200
     1.3 @@ -153,7 +153,7 @@
     1.4  subsubsection {* Small lazy typeclasses *}
     1.5  
     1.6  class small_lazy =
     1.7 -  fixes small_lazy :: "int \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
     1.8 +  fixes small_lazy :: "code_numeral \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
     1.9  
    1.10  instantiation unit :: small_lazy
    1.11  begin
    1.12 @@ -178,7 +178,7 @@
    1.13  termination 
    1.14    by (relation "measure (%(d, i). nat (d + 1 - i))") auto
    1.15  
    1.16 -definition "small_lazy d = small_lazy' d (- d)"
    1.17 +definition "small_lazy d = small_lazy' (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    1.18  
    1.19  instance ..
    1.20  
    1.21 @@ -197,7 +197,7 @@
    1.22  instantiation list :: (small_lazy) small_lazy
    1.23  begin
    1.24  
    1.25 -fun small_lazy_list :: "int => 'a list Lazy_Sequence.lazy_sequence"
    1.26 +fun small_lazy_list :: "code_numeral => 'a list Lazy_Sequence.lazy_sequence"
    1.27  where
    1.28    "small_lazy_list d = Lazy_Sequence.append (Lazy_Sequence.single []) (if d > 0 then Lazy_Sequence.bind (product (small_lazy (d - 1)) (small_lazy (d - 1))) (%(x, xs). Lazy_Sequence.single (x # xs)) else Lazy_Sequence.empty)"
    1.29