--- 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 =