formally stylized
authorhaftmann
Fri Aug 14 15:36:54 2009 +0200 (2009-08-14)
changeset 32372b0d2b49bfaed
parent 32371 3186fa3a4f88
child 32373 c96330408d89
formally stylized
src/HOL/Predicate.thy
     1.1 --- a/src/HOL/Predicate.thy	Fri Aug 14 15:36:53 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Fri Aug 14 15:36:54 2009 +0200
     1.3 @@ -646,7 +646,7 @@
     1.4  @{code_datatype pred = Seq};
     1.5  @{code_datatype seq = Empty | Insert | Join};
     1.6  
     1.7 -fun yield (Seq f) = next (f ())
     1.8 +fun yield (@{code Seq} f) = next (f ())
     1.9  and next @{code Empty} = NONE
    1.10    | next (@{code Insert} (x, P)) = SOME (x, P)
    1.11    | next (@{code Join} (P, xq)) = (case yield P