# HG changeset patch
# User wenzelm
# Date 1288780431 -3600
# Node ID 035b2afbeb2e3ca901c23bf1c3d091ff327103f7
# Parent  1eac228c52b3f852ec1161f490ac5ef33b9262d9
discontinued obsolete function sys_error and exception SYS_ERROR;

diff -r 1eac228c52b3 -r 035b2afbeb2e NEWS
--- 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.
diff -r 1eac228c52b3 -r 035b2afbeb2e src/Pure/Isar/runtime.ML
--- 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) =>
diff -r 1eac228c52b3 -r 035b2afbeb2e src/Pure/library.ML
--- 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;