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