# HG changeset patch
# User wenzelm
# Date 1184358970 -7200
# Node ID d67aac3992c37e4a968cb62d0ea3dd19fa105939
# Parent  953eb3c5f79394fbaee7522b3a6f089144311405
tuned;

diff -r 953eb3c5f793 -r d67aac3992c3 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Jul 12 12:20:39 2007 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Jul 13 22:36:10 2007 +0200
@@ -470,9 +470,8 @@
 
     fun lost_structure () = error ("Lost goal structure:\n" ^ string_of_thm goal);
 
-    val ns = map length propss;
     val th = Goal.conclude
-      (if Library.foldl op + (0, ns) > 1 then Thm.norm_proof goal else goal)
+      (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
       handle THM _ => lost_structure ();
     val goal_propss = filter_out null propss;
     val results =