src/Pure/Isar/proof_display.ML

   | subgoals n = [Pretty.brk 1, Pretty.str ("(" ^ string_of_int n ^ " subgoals)")];
 
 in
 
 fun pretty_goal_header goal =
-  Pretty.block ([Pretty.command "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]);
+  Pretty.block ([Pretty.keyword1 "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]);
 
 end;
 
 fun string_of_goal ctxt goal =
   Pretty.string_of (Pretty.chunks [pretty_goal_header goal, Goal_Display.pretty_goal ctxt goal]);

 (* goal facts *)
 
 fun pretty_goal_facts ctxt s ths =
   (Pretty.block o Pretty.fbreaks)
     [if s = "" then Pretty.str "this:"
-     else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"],
+     else Pretty.block [Pretty.keyword1 s, Pretty.brk 1, Pretty.str "this:"],
      Proof_Context.pretty_fact ctxt ("", ths)];
 
 
 (* method_error *)
 

 
 (* results *)
 
 local
 
-fun pretty_fact_name (kind, "") = Pretty.command kind
+fun pretty_fact_name (kind, "") = Pretty.keyword1 kind
   | pretty_fact_name (kind, name) =
-      Pretty.block [Pretty.command kind, Pretty.brk 1,
+      Pretty.block [Pretty.keyword1 kind, Pretty.brk 1,
         Pretty.str (Long_Name.base_name name), Pretty.str ":"];
 
 fun pretty_facts ctxt =
-  flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o
+  flat o (separate [Pretty.fbrk, Pretty.keyword2 "and", Pretty.str " "]) o
     map (single o Proof_Context.pretty_fact ctxt);
 
 in
 
 fun print_results markup do_print ctxt ((kind, name), facts) =
   if not do_print orelse kind = "" then ()
   else if name = "" then
     (Pretty.writeln o Pretty.mark markup)
-      (Pretty.block (Pretty.command kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
+      (Pretty.block (Pretty.keyword1 kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
   else
     (Pretty.writeln o Pretty.mark markup)
       (case facts of
         [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
           Proof_Context.pretty_fact ctxt fact])