src/Pure/Isar/proof.ML
changeset 8239 07f25f7d2218
parent 8234 36a85a6c4852
child 8374 ffb2eb084078
     1.1 --- a/src/Pure/Isar/proof.ML	Sun Feb 13 21:01:26 2000 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Mon Feb 14 11:23:44 2000 +0100
     1.3 @@ -264,7 +264,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 proof command in " ^ mode_name mode ^ " mode", state)
     1.8 +    else raise STATE ("Illegal application of command in " ^ mode_name mode ^ " mode", state)
     1.9    end;
    1.10  
    1.11  fun is_chain state = get_mode state = ForwardChain;