# HG changeset patch
# User wenzelm
# Date 1302990118 -7200
# Node ID fb539d6d1ac25901dad56596dc37d37a8660ee3d
# Parent  6cca8d2a79ad1d4de3be3630cdbdef3099abab1c
PARALLEL_GOALS for simplification within auto_tac;

diff -r 6cca8d2a79ad -r fb539d6d1ac2 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Sat Apr 16 23:41:25 2011 +0200
+++ b/src/Provers/clasimp.ML	Sat Apr 16 23:41:58 2011 +0200
@@ -201,7 +201,7 @@
           blast_depth_tac cs m               (* fast but can't use wrappers *)
           ORELSE'
           (CHANGED o nodup_depth_tac cs' n); (* slower but more general *)
-    in  EVERY [ALLGOALS (Simplifier.asm_full_simp_tac ss),
+    in  EVERY [PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac ss)),
                TRY (Classical.safe_tac cs),
                REPEAT_DETERM (FIRSTGOAL maintac),
                TRY (Classical.safe_tac (cs addSss ss)),