src/Pure/Isar/toplevel.ML
changeset 6002 c1f28f8ec72c
parent 5990 8b6de9bd7d72
child 6194 358f62acf573
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Dec 01 14:46:58 1998 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Dec 01 14:47:26 1998 +0100
     1.3 @@ -254,6 +254,7 @@
     1.4    | exn_message (BREAK _) = "Break."
     1.5    | exn_message (FAIL (exn, msg)) = cat_lines [exn_message exn, msg]
     1.6    | exn_message Interrupt = "Interrupt (exec)."
     1.7 +  | exn_message ERROR = "ERROR."
     1.8    | exn_message (ERROR_MESSAGE msg) = msg
     1.9    | exn_message (THEORY (msg, _)) = msg
    1.10    | exn_message (ProofContext.CONTEXT (msg, _)) = msg
    1.11 @@ -341,7 +342,7 @@
    1.12  fun excursion trs =
    1.13    (case excur trs (State []) of
    1.14      State [] => ()
    1.15 -  | _ => error "Pending blocks at end of excursion");
    1.16 +  | _ => raise ERROR_MESSAGE "Pending blocks at end of excursion");
    1.17  
    1.18  
    1.19