PARALLEL_GOALS for simplification within auto_tac;
authorwenzelm
Sat, 16 Apr 2011 23:41:58 +0200
changeset 42373 fb539d6d1ac2
parent 42372 6cca8d2a79ad
child 42374 b9a6b465da25
PARALLEL_GOALS for simplification within auto_tac;
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)),