--- a/NEWS Wed Nov 03 11:11:49 2010 +0100
+++ b/NEWS Wed Nov 03 11:33:51 2010 +0100
@@ -349,6 +349,10 @@
*** ML ***
+* Discontinued obsolete function sys_error and exception SYS_ERROR.
+See implementation manual for further details on exceptions in
+Isabelle/ML.
+
* Antiquotation @{assert} inlines a function bool -> unit that raises
Fail if the argument is false. Due to inlining the source position of
failed assertions is included in the error output.
--- a/src/Pure/Isar/runtime.ML Wed Nov 03 11:11:49 2010 +0100
+++ b/src/Pure/Isar/runtime.ML Wed Nov 03 11:33:51 2010 +0100
@@ -68,7 +68,6 @@
| TERMINATE => ["Exit"]
| TimeLimit.TimeOut => ["Timeout"]
| TOPLEVEL_ERROR => ["Error"]
- | SYS_ERROR msg => ["## SYSTEM ERROR ##\n" ^ msg]
| ERROR msg => [msg]
| Fail msg => [raised exn "Fail" [msg]]
| THEORY (msg, thys) =>
--- a/src/Pure/library.ML Wed Nov 03 11:11:49 2010 +0100
+++ b/src/Pure/library.ML Wed Nov 03 11:33:51 2010 +0100
@@ -29,8 +29,6 @@
val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a
(*errors*)
- exception SYS_ERROR of string
- val sys_error: string -> 'a
exception ERROR of string
val error: string -> 'a
val cat_error: string -> string -> 'a
@@ -256,11 +254,9 @@
fun funpow_yield (0 : int) _ x = ([], x)
| funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
+
(* errors *)
-exception SYS_ERROR of string;
-fun sys_error msg = raise SYS_ERROR msg;
-
exception ERROR of string;
fun error msg = raise ERROR msg;