src/HOL/Lazy_Sequence.thy
changeset 45214 66ba67adafab
parent 42163 392fd6c4669c
child 50055 94041d602ecb
--- a/src/HOL/Lazy_Sequence.thy	Thu Oct 20 08:20:35 2011 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Thu Oct 20 09:11:13 2011 +0200
@@ -153,7 +153,7 @@
 subsubsection {* Small lazy typeclasses *}
 
 class small_lazy =
-  fixes small_lazy :: "int \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
+  fixes small_lazy :: "code_numeral \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
 
 instantiation unit :: small_lazy
 begin
@@ -178,7 +178,7 @@
 termination 
   by (relation "measure (%(d, i). nat (d + 1 - i))") auto
 
-definition "small_lazy d = small_lazy' d (- d)"
+definition "small_lazy d = small_lazy' (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
 
 instance ..
 
@@ -197,7 +197,7 @@
 instantiation list :: (small_lazy) small_lazy
 begin
 
-fun small_lazy_list :: "int => 'a list Lazy_Sequence.lazy_sequence"
+fun small_lazy_list :: "code_numeral => 'a list Lazy_Sequence.lazy_sequence"
 where
   "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)"