1.1 --- a/src/HOL/ex/Predicate_Compile.thy	Mon Apr 20 09:32:07 2009 +0200
     1.2 +++ b/src/HOL/ex/Predicate_Compile.thy	Mon Apr 20 09:32:09 2009 +0200
     1.3 @@ -12,26 +12,21 @@
     1.4    | "next yield (Predicate.Join P xq) = (case yield P
     1.5     of None \<Rightarrow> next yield xq | Some (x, Q) \<Rightarrow> Some (x, Predicate.Seq (\<lambda>_. Predicate.Join Q xq)))"
     1.6  
     1.7 -ML {*
     1.8 -let
     1.9 -  fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ())
    1.10 -in
    1.11 -  yield @{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*)
    1.12 -end
    1.13 -*}
    1.14 -
    1.15  fun anamorph :: "('b \<Rightarrow> ('a \<times> 'b) option) \<Rightarrow> index \<Rightarrow> 'b \<Rightarrow> 'a list \<times> 'b" where
    1.16    "anamorph f k x = (if k = 0 then ([], x)
    1.17      else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow> let (vs, z) = anamorph f (k - 1) y in (v # vs, z))"
    1.18  
    1.19  ML {*
    1.20 -let
    1.21 -  fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ())
    1.22 -  fun yieldn k = @{code anamorph} yield k
    1.23 -in
    1.24 -  yieldn 0 (*replace with number of elements to retrieve*)
    1.25 -    @{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*)
    1.26 -end
    1.27 +structure Predicate =
    1.28 +struct
    1.29 +
    1.30 +open Predicate;
    1.31 +
    1.32 +fun yield (Predicate.Seq f) = @{code next} yield (f ());
    1.33 +
    1.34 +fun yieldn k = @{code anamorph} yield k;
    1.35 +
    1.36 +end;
    1.37  *}
    1.38  
    1.39  end
    1.40 \ No newline at end of file