# HG changeset patch
# User wenzelm
# Date 1325243536 -3600
# Node ID 9933bb0cc8afc1320bf743ec6f72ea57277e0bbc
# Parent  963af563a1328190a7768b99025b85878b701dbf
more parallelism;

diff -r 963af563a132 -r 9933bb0cc8af src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Dec 30 12:00:10 2011 +0100
+++ b/src/HOL/Tools/record.ML	Fri Dec 30 12:12:16 2011 +0100
@@ -2123,16 +2123,14 @@
     (* 3rd stage: thms_thy *)
 
     val ss = get_simpset defs_thy;
-    val simp_defs_tac =
-      asm_full_simp_tac (ss addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms));
-
-    val sel_convs = timeit_msg ctxt "record sel_convs proof:" (fn () =>
-      map (fn prop =>
-        Skip_Proof.prove_global defs_thy [] [] prop (K (ALLGOALS simp_defs_tac))) sel_conv_props);
-
-    val upd_convs = timeit_msg ctxt "record upd_convs proof:" (fn () =>
-      map (fn prop =>
-        Skip_Proof.prove_global defs_thy [] [] prop (K (ALLGOALS simp_defs_tac))) upd_conv_props);
+    val sel_upd_ss = ss addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms);
+
+    val (sel_convs, upd_convs) =
+      timeit_msg ctxt "record sel_convs/upd_convs proof:" (fn () =>
+        Par_List.map (fn prop =>
+          Skip_Proof.prove_global defs_thy [] [] prop
+            (K (ALLGOALS (asm_full_simp_tac sel_upd_ss)))) (sel_conv_props @ upd_conv_props))
+      |> chop (length sel_conv_props);
 
     val (fold_congs, unfold_congs) = timeit_msg ctxt "record upd fold/unfold congs:" (fn () =>
       let
@@ -2252,7 +2250,7 @@
             st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 THEN
               res_inst_tac context [((rN, 0), s')] cases_scheme 1 THEN
               Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1)
-             (*simp_defs_tac would also work but is less efficient*)
+             (*asm_full_simp_tac sel_upd_ss would also work but is less efficient*)
           end));
 
     val ((([sel_convs', upd_convs', sel_defs', upd_defs',