tuned msg;
authorwenzelm
Mon Apr 17 14:04:46 2000 +0200 (2000-04-17)
changeset 8722f745b34dcde3
parent 8721 453b493ece0a
child 8723 c7de3c2ed7a9
tuned msg;
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Mon Apr 17 14:03:51 2000 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Mon Apr 17 14:04:46 2000 +0200
     1.3 @@ -267,7 +267,7 @@
     1.4  fun assert_mode pred state =
     1.5    let val mode = get_mode state in
     1.6      if pred mode then state
     1.7 -    else raise STATE ("Illegal application of command in " ^ mode_name mode ^ " mode", state)
     1.8 +    else raise STATE ("Illegal application of proof command in " ^ mode_name mode ^ " mode", state)
     1.9    end;
    1.10  
    1.11  fun is_chain state = get_mode state = ForwardChain;
     2.1 --- a/src/Pure/Isar/toplevel.ML	Mon Apr 17 14:03:51 2000 +0200
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Apr 17 14:04:46 2000 +0200
     2.3 @@ -385,7 +385,7 @@
     2.4    let
     2.5      val _ =
     2.6        if int orelse not int_only then ()
     2.7 -      else warning (command_msg "Executing interactive-only " tr);
     2.8 +      else warning (command_msg "Interactive-only " tr);
     2.9      val (result, opt_exn) =
    2.10        (if ! trace then (writeln (command_msg "" tr); timeap) else I) (apply_trans int trans) state;
    2.11      val _ = if int andalso print andalso not (! quiet) then print_state result else ();