tuned print_state;
authorwenzelm
Sat Jul 03 00:23:17 1999 +0200 (1999-07-03)
changeset 68917bb02d03035d
parent 6890 05732285677e
child 6892 4a905b4a39c8
tuned print_state;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Sat Jul 03 00:22:53 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Sat Jul 03 00:23:17 1999 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4    val goal_facts: (state -> thm list) -> state -> state
     1.5    val use_facts: state -> state
     1.6    val reset_facts: state -> state
     1.7 +  val assert_forward: state -> state
     1.8    val assert_backward: state -> state
     1.9    val enter_forward: state -> state
    1.10    val verbose: bool ref
    1.11 @@ -280,7 +281,7 @@
    1.12  
    1.13      val ctxt_strings = ProofContext.strings_of_context context;
    1.14    in
    1.15 -    writeln ("Nesting level: " ^ string_of_int (length nodes div 2));
    1.16 +    if ! verbose then writeln ("Nesting level: " ^ string_of_int (length nodes div 2)) else ();
    1.17      writeln "";
    1.18      writeln (mode_name mode ^ " mode");
    1.19      writeln "";