src/Pure/Isar/proof.ML
changeset 23782 4dd0ba632e40
parent 23639 961d1061e540
child 23806 d67aac3992c3
equal deleted inserted replaced
23781:ab793a6ddf9f 23782:4dd0ba632e40
   468     val _ = null extra_hyps orelse
   468     val _ = null extra_hyps orelse
   469       error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term extra_hyps));
   469       error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term extra_hyps));
   470 
   470 
   471     fun lost_structure () = error ("Lost goal structure:\n" ^ string_of_thm goal);
   471     fun lost_structure () = error ("Lost goal structure:\n" ^ string_of_thm goal);
   472 
   472 
   473     val th = Goal.conclude goal handle THM _ => lost_structure ();
   473     val ns = map length propss;
       
   474     val th = Goal.conclude
       
   475       (if Library.foldl op + (0, ns) > 1 then Thm.norm_proof goal else goal)
       
   476       handle THM _ => lost_structure ();
   474     val goal_propss = filter_out null propss;
   477     val goal_propss = filter_out null propss;
   475     val results =
   478     val results =
   476       Conjunction.elim_balanced (length goal_propss) th
   479       Conjunction.elim_balanced (length goal_propss) th
   477       |> map2 Conjunction.elim_balanced (map length goal_propss)
   480       |> map2 Conjunction.elim_balanced (map length goal_propss)
   478       handle THM _ => lost_structure ();
   481       handle THM _ => lost_structure ();