more elegant ML
authorblanchet
Wed, 01 Sep 2010 21:47:25 +0200
changeset 39001 42e6eb597c30
parent 39000 d73a054e018c
child 39002 a2d7be688ea1
more elegant ML
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) =