src/Pure/goal_display.ML
changeset 50201 c26369c9eda6
parent 49847 ed5080c03165
child 50537 08ce81aeeacc
equal deleted inserted replaced
50200:2c94c065564e 50201:c26369c9eda6
   114 
   114 
   115     fun pretty_list _ _ [] = []
   115     fun pretty_list _ _ [] = []
   116       | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
   116       | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
   117 
   117 
   118     fun pretty_subgoal (n, A) =
   118     fun pretty_subgoal (n, A) =
   119       Pretty.markup Isabelle_Markup.subgoal
   119       Pretty.markup Markup.subgoal [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
   120         [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
       
   121     fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
   120     fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
   122 
   121 
   123     val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
   122     val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
   124 
   123 
   125     val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
   124     val pretty_consts = pretty_list "constants:" prt_consts o consts_of;