src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Fri Sep 04 19:22:13 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Fri Sep 04 21:40:59 2015 +0200
@@ -76,6 +76,7 @@
     fun proves goals = goals
       |> Logic.mk_conjunction_balanced
       |> prove
+      |> Thm.close_derivation
       |> Conjunction.elim_balanced (length goals)
       |> map Simpdata.mk_eq;
   in