1.1 --- a/src/HOL/Code_Numeral.thy	Fri Feb 24 22:46:16 2012 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Feb 24 22:46:44 2012 +0100
     1.3 @@ -281,18 +281,7 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -text {* Lazy Evaluation of an indexed function *}
     1.8 -
     1.9 -function iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a Predicate.pred"
    1.10 -where
    1.11 -  "iterate_upto f n m =
    1.12 -    Predicate.Seq (%u. if n > m then Predicate.Empty
    1.13 -     else Predicate.Insert (f n) (iterate_upto f (n + 1) m))"
    1.14 -by pat_completeness auto
    1.15 -
    1.16 -termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
    1.17 -
    1.18 -hide_const (open) of_nat nat_of Suc  subtract int_of iterate_upto
    1.19 +hide_const (open) of_nat nat_of Suc subtract int_of
    1.20  
    1.21  
    1.22  subsection {* Code generator setup *}
    1.23 @@ -377,3 +366,4 @@
    1.24    Code_Numeral Arith
    1.25  
    1.26  end
    1.27 +