# HG changeset patch
# User haftmann
# Date 1257926540 -3600
# Node ID 9b3c4e95380e920da49365e2b20c704e96bb967e
# Parent  2b27020ffcb2d190bd7d8fd7c1f4b235aa9d9bb2
tuned

diff -r 2b27020ffcb2 -r 9b3c4e95380e src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed Nov 11 00:11:26 2009 +0100
+++ b/src/HOL/Predicate.thy	Wed Nov 11 09:02:20 2009 +0100
@@ -802,14 +802,14 @@
   | next (@{code Insert} (x, P)) = SOME (x, P)
   | next (@{code Join} (P, xq)) = (case yield P
      of NONE => next xq
-      | SOME (x, Q) => SOME (x, @{code Seq} (fn _ => @{code Join} (Q, xq))))
+      | SOME (x, Q) => SOME (x, @{code Seq} (fn _ => @{code Join} (Q, xq))));
 
 fun anamorph f k x = (if k = 0 then ([], x)
   else case f x
    of NONE => ([], x)
     | SOME (v, y) => let
         val (vs, z) = anamorph f (k - 1) y
-      in (v :: vs, z) end)
+      in (v :: vs, z) end);
 
 fun yieldn P = anamorph yield P;