1.1 --- a/src/Pure/Isar/proof.ML	Thu Mar 23 11:28:10 2000 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Mar 23 21:36:43 2000 +0100
     1.3 @@ -329,8 +329,9 @@
     1.4        else [];
     1.5  
     1.6      val prts =
     1.7 -     [Pretty.str ("Proof(" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
     1.8 -        ", depth " ^ string_of_int (length nodes div 2)), Pretty.str ""] @
     1.9 +     [Pretty.str ("proof(" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
    1.10 +        (if ! verbose then ", depth " ^ string_of_int (length nodes div 2)
    1.11 +        else "")), Pretty.str ""] @
    1.12       (if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @
    1.13       (if ! verbose orelse mode = Forward then
    1.14         (pretty_facts "" facts @ pretty_goal (find_goal 0 state))

     2.1 --- a/src/Pure/Isar/toplevel.ML	Thu Mar 23 11:28:10 2000 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Mar 23 21:36:43 2000 +0100
     2.3 @@ -80,7 +80,7 @@
     2.4    | str_of_node (Proof _) = "in proof mode";
     2.5  
     2.6  fun print_ctxt thy = Pretty.writeln (Pretty.block
     2.7 -  [Pretty.str "Theory:", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
     2.8 +  [Pretty.str "theory", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
     2.9      Pretty.str " =", Pretty.brk 1, Display.pretty_theory thy]);
    2.10  
    2.11  fun print_node_ctxt (Theory thy) = print_ctxt thy