# HG changeset patch
# User wenzelm
# Date 1436893306 -7200
# Node ID 757cad5a3fe9a38ef5ee3022e6833d547c0a2fcb
# Parent  a8babbb6d5eaf542a0500e95b12af4633d0f49da
more aggressive compaction of multi-goal proof terms (see also a8babbb6d5ea, 4dd0ba632e40);

diff -r a8babbb6d5ea -r 757cad5a3fe9 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Jul 14 11:29:43 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jul 14 19:01:46 2015 +0200
@@ -498,7 +498,7 @@
     fun err_lost () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal);
 
     val th =
-      (Goal.conclude (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
+      (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
         handle THM _ => err_lost ())
       |> Drule.flexflex_unique (SOME ctxt)
       |> Thm.check_shyps (Variable.sorts_of ctxt)
diff -r a8babbb6d5ea -r 757cad5a3fe9 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue Jul 14 11:29:43 2015 +0200
+++ b/src/Pure/goal.ML	Tue Jul 14 19:01:46 2015 +0200
@@ -231,7 +231,7 @@
           (Thm.term_of stmt);
   in
     res
-    |> length props > 1 ? Thm.norm_proof
+    |> length props > 1 ? Thm.close_derivation
     |> Conjunction.elim_balanced (length props)
     |> map (Assumption.export false ctxt' ctxt)
     |> Variable.export ctxt' ctxt