1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Mon Jun 29 14:55:08 2009 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon Jun 29 16:17:55 2009 +0200
     1.3 @@ -450,7 +450,7 @@
     1.4  qed
     1.5  
     1.6  lemma [code]:
     1.7 -  "iter f step ss w = while (\<lambda>(ss, w). \<not> (is_empty w))
     1.8 +  "iter f step ss w = while (\<lambda>(ss, w). \<not> is_empty w)
     1.9      (\<lambda>(ss, w).
    1.10          let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
    1.11      (ss, w)"