# HG changeset patch
# User wenzelm
# Date 1302990085 -7200
# Node ID 6cca8d2a79ad1d4de3be3630cdbdef3099abab1c
# Parent  5900f06b41986deb84723de3039aafbdb63af09b
PARALLEL_GOALS for method "simp_all";

diff -r 5900f06b4198 -r 6cca8d2a79ad src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sat Apr 16 23:38:25 2011 +0200
+++ b/src/Pure/simplifier.ML	Sat Apr 16 23:41:25 2011 +0200
@@ -394,7 +394,7 @@
   Method.setup (Binding.name "simp_all")
     (simp_method more_mods (fn ctxt => fn tac => fn facts =>
       ALLGOALS (Method.insert_tac facts) THEN
-        (CHANGED_PROP o ALLGOALS o tac) (simpset_of ctxt)))
+        (CHANGED_PROP o PARALLEL_GOALS o ALLGOALS o tac) (simpset_of ctxt)))
     "simplification (all goals)";
 
 fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn _ =>