Proof terms for meta-conjunctions are now normalized before
splitting up the conjunctions.

--- a/src/Pure/Isar/proof.ML	Wed Jul 11 11:59:21 2007 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Jul 11 12:01:10 2007 +0200
@@ -470,7 +470,10 @@
 
     fun lost_structure () = error ("Lost goal structure:\n" ^ string_of_thm goal);
 
-    val th = Goal.conclude goal handle THM _ => lost_structure ();
+    val ns = map length propss;
+    val th = Goal.conclude
+      (if Library.foldl op + (0, ns) > 1 then Thm.norm_proof goal else goal)
+      handle THM _ => lost_structure ();
     val goal_propss = filter_out null propss;
     val results =
       Conjunction.elim_balanced (length goal_propss) th