# HG changeset patch
# User traytel
# Date 1428923021 -7200
# Node ID 894d6d863823c0fbf187f0f62cee3879cb43de54
# Parent  cd2b6debac181cac0b05a282dfb327d0f6fc8f1c
call Goal.prove only once for a quadratic number of theorems

diff -r cd2b6debac18 -r 894d6d863823 src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
--- 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 =