# HG changeset patch
# User haftmann
# Date 1250257014 -7200
# Node ID b0d2b49bfaede2a0e37d49e62f97539d30d463e3
# Parent  3186fa3a4f88bd71d3d4dd06bde1e3ab74e77403
formally stylized

diff -r 3186fa3a4f88 -r b0d2b49bfaed src/HOL/Predicate.thy
--- 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