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