author traytel Mon Apr 13 13:03:41 2015 +0200 (2015-04-13) changeset 60046 894d6d863823 parent 60045 cd2b6debac18 child 60056 71c1b9b9e937 child 60057 86fa63ce8156
call Goal.prove only once for a quadratic number of theorems
```     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon Apr 13 12:15:29 2015 +0200
1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon Apr 13 13:03:41 2015 +0200
1.3 @@ -68,12 +68,18 @@
1.4
1.5      fun prove goal =
1.6        Goal.prove_sorry_global thy [] [] goal (fn {context = ctxt, ...} =>
1.8          ALLGOALS (simp_tac
1.9            (put_simpset HOL_basic_ss ctxt
1.10 -            addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms)))))
1.11 -      |> Simpdata.mk_eq;
1.12 +            addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms)))));
1.13 +
1.14 +    fun proves goals = goals
1.15 +      |> Logic.mk_conjunction_balanced
1.16 +      |> prove
1.17 +      |> Conjunction.elim_balanced (length goals)
1.18 +      |> map Simpdata.mk_eq;
1.19    in
1.20 -    (map prove (triv_inject_goals @ inject_goals @ distinct_goals), prove refl_goal)
1.21 +    (proves (triv_inject_goals @ inject_goals @ distinct_goals), Simpdata.mk_eq (prove refl_goal))
1.22    end;
1.23
1.24  fun add_equality fcT fcT_name As ctrs inject_thms distinct_thms =
```