author | wenzelm |
Sat, 16 Apr 2011 23:38:25 +0200 | |
changeset 42371 | 5900f06b4198 |
parent 42370 | 244911efd275 |
child 42372 | 6cca8d2a79ad |
src/Pure/goal.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/goal.ML Sat Apr 16 22:21:34 2011 +0200 +++ b/src/Pure/goal.ML Sat Apr 16 23:38:25 2011 +0200 @@ -347,7 +347,7 @@ fun PARALLEL_GOALS tac = Thm.adjust_maxidx_thm ~1 #> (fn st => - if not (future_enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1 + if not (Multithreading.enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1 then DETERM tac st else let