tuned goal output;
authorwenzelm
Tue, 31 Oct 2000 20:33:10 +0100
changeset 10364 eacd2685c0db
parent 10363 6e8002c1790e
child 10365 a17cf465d29a
tuned goal output;
src/Pure/locale.ML
--- a/src/Pure/locale.ML	Tue Oct 31 13:59:41 2000 +0100
+++ b/src/Pure/locale.ML	Tue Oct 31 20:33:10 2000 +0100
@@ -620,11 +620,11 @@
         Pretty.blk (0, [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), prt_term A]);
       fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
 
-      val pretty_ffpairs = pretty_list "Flex-flex pairs:" (prt_term o Logic.mk_flexpair);
+      val pretty_ffpairs = pretty_list "flex-flex pairs:" (prt_term o Logic.mk_flexpair);
 
-      val pretty_consts = pretty_list "Constants:" prt_consts o consts_of;
-      val pretty_vars = pretty_list "Variables:" prt_vars o vars_of;
-      val pretty_varsT = pretty_list "Type variables:" prt_varsT o varsT_of;
+      val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
+      val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
+      val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
 
 
       val {prop, ...} = rep_thm state;