--- a/src/Pure/goal_display.ML Fri Dec 14 18:41:56 2012 +0100
+++ b/src/Pure/goal_display.ML Fri Dec 14 20:05:08 2012 +0100
@@ -115,9 +115,9 @@
fun pretty_list _ _ [] = []
| pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
- fun pretty_subgoal (n, A) =
- Pretty.markup Markup.subgoal [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
- fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
+ fun pretty_subgoal s A =
+ Pretty.markup (Markup.subgoal s) [Pretty.str (" " ^ s ^ ". "), prt_term A];
+ val pretty_subgoals = map_index (fn (i, A) => pretty_subgoal (string_of_int (i + 1)) A);
val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);