src/Pure/Isar/proof.ML
changeset 23806 d67aac3992c3
parent 23782 4dd0ba632e40
child 23963 c2ee97a963db
equal deleted inserted replaced
23805:953eb3c5f793 23806:d67aac3992c3
   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 ns = map length propss;
       
   474     val th = Goal.conclude
   473     val th = Goal.conclude
   475       (if Library.foldl op + (0, ns) > 1 then Thm.norm_proof goal else goal)
   474       (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
   476       handle THM _ => lost_structure ();
   475       handle THM _ => lost_structure ();
   477     val goal_propss = filter_out null propss;
   476     val goal_propss = filter_out null propss;
   478     val results =
   477     val results =
   479       Conjunction.elim_balanced (length goal_propss) th
   478       Conjunction.elim_balanced (length goal_propss) th
   480       |> map2 Conjunction.elim_balanced (map length goal_propss)
   479       |> map2 Conjunction.elim_balanced (map length goal_propss)