# HG changeset patch
# User blanchet
# Date 1283370445 -7200
# Node ID 42e6eb597c30e060d52758515493194ef55453bf
# Parent  d73a054e018c467a4a279b52addc3a27d68dc2fe
more elegant ML

diff -r d73a054e018c -r 42e6eb597c30 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Sep 01 18:47:07 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Sep 01 21:47:25 2010 +0200
@@ -348,7 +348,7 @@
                            |>> curry (op =) "genuine")
   in
     if auto orelse blocking then go ()
-    else (Toplevel.thread true (fn () => (go (); ())); (false, state))
+    else (Toplevel.thread true (tap go); (false, state))
   end
 
 fun nitpick_trans (params, i) =