src/Pure/Isar/proof.ML
changeset 24550 ec228ae5a620
parent 24543 e2332d1ff6c7
child 24556 22ac3c8d78a5
equal deleted inserted replaced
24549:c8cee92b06bc 24550:ec228ae5a620
   337 
   337 
   338     fun description strs =
   338     fun description strs =
   339       (case filter_out (equal "") strs of [] => ""
   339       (case filter_out (equal "") strs of [] => ""
   340       | strs' => enclose " (" ")" (commas strs'));
   340       | strs' => enclose " (" ")" (commas strs'));
   341 
   341 
   342     fun prt_goal (SOME (ctxt, (i, {messages, using, goal, before_qed, after_qed, ...}))) =
   342     fun prt_goal (SOME (ctxt, (i,
       
   343             {statement = _, messages, using, goal, before_qed, after_qed}))) =
   343           pretty_facts "using " ctxt
   344           pretty_facts "using " ctxt
   344             (if mode <> Backward orelse null using then NONE else SOME using) @
   345             (if mode <> Backward orelse null using then NONE else SOME using) @
   345           [Pretty.str ("goal" ^
   346           [Pretty.str ("goal" ^
   346             description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
   347             description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
   347           pretty_goals_local ctxt Markup.subgoal
   348           pretty_goals_local ctxt Markup.subgoal