tuned
authorhaftmann
Wed Nov 11 09:02:20 2009 +0100 (2009-11-11)
changeset 336079b3c4e95380e
parent 33606 2b27020ffcb2
child 33608 5c0024338cef
tuned
src/HOL/Predicate.thy
     1.1 --- a/src/HOL/Predicate.thy	Wed Nov 11 00:11:26 2009 +0100
     1.2 +++ b/src/HOL/Predicate.thy	Wed Nov 11 09:02:20 2009 +0100
     1.3 @@ -802,14 +802,14 @@
     1.4    | next (@{code Insert} (x, P)) = SOME (x, P)
     1.5    | next (@{code Join} (P, xq)) = (case yield P
     1.6       of NONE => next xq
     1.7 -      | SOME (x, Q) => SOME (x, @{code Seq} (fn _ => @{code Join} (Q, xq))))
     1.8 +      | SOME (x, Q) => SOME (x, @{code Seq} (fn _ => @{code Join} (Q, xq))));
     1.9  
    1.10  fun anamorph f k x = (if k = 0 then ([], x)
    1.11    else case f x
    1.12     of NONE => ([], x)
    1.13      | SOME (v, y) => let
    1.14          val (vs, z) = anamorph f (k - 1) y
    1.15 -      in (v :: vs, z) end)
    1.16 +      in (v :: vs, z) end);
    1.17  
    1.18  fun yieldn P = anamorph yield P;
    1.19