exn_message FAIL;
authorwenzelm
Wed Nov 18 11:12:29 1998 +0100 (1998-11-18)
changeset 593041aa67a045f7
parent 5929 890f2f9b926d
child 5931 325300576da7
exn_message FAIL;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Nov 18 11:03:49 1998 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Nov 18 11:12:29 1998 +0100
     1.3 @@ -233,6 +233,7 @@
     1.4  
     1.5  fun exn_message TERMINATE = "Exit."
     1.6    | exn_message (BREAK _) = "Break."
     1.7 +  | exn_message (FAIL (exn, msg)) = cat_lines [exn_message exn, msg]
     1.8    | exn_message Interrupt = "Interrupt (exec)."
     1.9    | exn_message (ERROR_MESSAGE msg) = msg
    1.10    | exn_message (THEORY (msg, _)) = msg