# HG changeset patch
# User haftmann
# Date 1240212729 -7200
# Node ID d5f5ab29d76907e5fa9a042380e9edf3b702322b
# Parent  7ab2716dd93b480af62accb0a6dc04254c0fc5d5
yield is now a static ML function

diff -r 7ab2716dd93b -r d5f5ab29d769 src/HOL/ex/Predicate_Compile.thy
--- a/src/HOL/ex/Predicate_Compile.thy	Mon Apr 20 09:32:07 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy	Mon Apr 20 09:32:09 2009 +0200
@@ -12,26 +12,21 @@
   | "next yield (Predicate.Join P xq) = (case yield P
    of None \<Rightarrow> next yield xq | Some (x, Q) \<Rightarrow> Some (x, Predicate.Seq (\<lambda>_. Predicate.Join Q xq)))"
 
-ML {*
-let
-  fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ())
-in
-  yield @{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*)
-end
-*}
-
 fun anamorph :: "('b \<Rightarrow> ('a \<times> 'b) option) \<Rightarrow> index \<Rightarrow> 'b \<Rightarrow> 'a list \<times> 'b" where
   "anamorph f k x = (if k = 0 then ([], x)
     else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow> let (vs, z) = anamorph f (k - 1) y in (v # vs, z))"
 
 ML {*
-let
-  fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ())
-  fun yieldn k = @{code anamorph} yield k
-in
-  yieldn 0 (*replace with number of elements to retrieve*)
-    @{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*)
-end
+structure Predicate =
+struct
+
+open Predicate;
+
+fun yield (Predicate.Seq f) = @{code next} yield (f ());
+
+fun yieldn k = @{code anamorph} yield k;
+
+end;
 *}
 
 end
\ No newline at end of file