| changeset 32372 | b0d2b49bfaed |
| parent 32235 | 8f9b8d14fc9f |
| child 32578 | 22117a76f943 |
--- a/src/HOL/Predicate.thy Fri Aug 14 15:36:53 2009 +0200 +++ b/src/HOL/Predicate.thy Fri Aug 14 15:36:54 2009 +0200 @@ -646,7 +646,7 @@ @{code_datatype pred = Seq}; @{code_datatype seq = Empty | Insert | Join}; -fun yield (Seq f) = next (f ()) +fun yield (@{code Seq} f) = next (f ()) and next @{code Empty} = NONE | next (@{code Insert} (x, P)) = SOME (x, P) | next (@{code Join} (P, xq)) = (case yield P