call Goal.prove only once for a quadratic number of theorems

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon Apr 13 12:15:29 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon Apr 13 13:03:41 2015 +0200
@@ -68,12 +68,18 @@
 
     fun prove goal =
       Goal.prove_sorry_global thy [] [] goal (fn {context = ctxt, ...} =>
+        HEADGOAL Goal.conjunction_tac THEN
         ALLGOALS (simp_tac
           (put_simpset HOL_basic_ss ctxt
-            addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms)))))
-      |> Simpdata.mk_eq;
+            addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms)))));
+
+    fun proves goals = goals
+      |> Logic.mk_conjunction_balanced
+      |> prove
+      |> Conjunction.elim_balanced (length goals)
+      |> map Simpdata.mk_eq;
   in
-    (map prove (triv_inject_goals @ inject_goals @ distinct_goals), prove refl_goal)
+    (proves (triv_inject_goals @ inject_goals @ distinct_goals), Simpdata.mk_eq (prove refl_goal))
   end;
 
 fun add_equality fcT fcT_name As ctrs inject_thms distinct_thms =