src/Pure/Isar/proof.ML
changeset 8722 f745b34dcde3
parent 8718 3ba75b7e1168
child 8807 0046be1769f9
     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;