src/HOL/Tools/Sledgehammer/sledgehammer.ML
changeset 39223 022f16801e4e
parent 39155 3e94ebe282f1
parent 39220 8420a873f534
child 39262 bdfcf2434601
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 08 14:46:21 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 08 16:01:06 2010 +0200
     1.3 @@ -452,8 +452,7 @@
     1.4              else
     1.5                ()
     1.6            end
     1.7 -      (* FIXME no threads in user-space *)
     1.8 -      in if blocking then run () else Toplevel.thread true (tap run) |> K () end
     1.9 +      in if blocking then run () else Future.fork run |> K () end
    1.10  
    1.11  val setup =
    1.12    dest_dir_setup