PARALLEL_GOALS for method "simp_all";
authorwenzelm
Sat, 16 Apr 2011 23:41:25 +0200
changeset 42372 6cca8d2a79ad
parent 42371 5900f06b4198
child 42373 fb539d6d1ac2
PARALLEL_GOALS for method "simp_all";
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 _ =>