# HG changeset patch # User berghofe # Date 1184148070 -7200 # Node ID 4dd0ba632e404874066b2f335e7a331e59c12555 # Parent ab793a6ddf9fc38cd9672a2c530b25516bc46168 Proof terms for meta-conjunctions are now normalized before splitting up the conjunctions. diff -r ab793a6ddf9f -r 4dd0ba632e40 src/Pure/Isar/proof.ML --- 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