src/Pure/simplifier.ML
changeset 42372 6cca8d2a79ad
parent 42360 da8817d01e7c
child 42375 774df7c59508
--- 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 _ =>