# HG changeset patch
# User wenzelm
# Date 1288778782 -3600
# Node ID 665862241968d9be88d90b96002b1f11dbcc3acb
# Parent  11846d9800de5aceaad127b46abb9fcf23293c4a
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;

diff -r 11846d9800de -r 665862241968 src/HOL/Library/Eval_Witness.thy
--- a/src/HOL/Library/Eval_Witness.thy	Wed Nov 03 10:51:40 2010 +0100
+++ b/src/HOL/Library/Eval_Witness.thy	Wed Nov 03 11:06:22 2010 +0100
@@ -63,7 +63,7 @@
   fun dest_exs  0 t = t
     | dest_exs n (Const (@{const_name Ex}, _) $ Abs (v,T,b)) = 
       Abs (v, check_type T, dest_exs (n - 1) b)
-    | dest_exs _ _ = sys_error "dest_exs";
+    | dest_exs _ _ = raise Fail "dest_exs";
   val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
 in
   if Code_Runtime.dynamic_value_strict (Eval_Method.get, Eval_Method.put, "Eval_Method.put") thy NONE (K I) t ws
diff -r 11846d9800de -r 665862241968 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Nov 03 10:51:40 2010 +0100
+++ b/src/HOL/Tools/inductive.ML	Wed Nov 03 11:06:22 2010 +0100
@@ -229,7 +229,7 @@
 
 fun arg_types_of k c = drop k (binder_types (fastype_of c));
 
-fun find_arg T x [] = sys_error "find_arg"
+fun find_arg T x [] = raise Fail "find_arg"
   | find_arg T x ((p as (_, (SOME _, _))) :: ps) =
       apsnd (cons p) (find_arg T x ps)
   | find_arg T x ((p as (U, (NONE, y))) :: ps) =
diff -r 11846d9800de -r 665862241968 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Nov 03 10:51:40 2010 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Nov 03 11:06:22 2010 +0100
@@ -327,8 +327,8 @@
 
 fun multiply_ineq n (i as Lineq(k,ty,l,just)) =
   if n = 1 then i
-  else if n = 0 andalso ty = Lt then sys_error "multiply_ineq"
-  else if n < 0 andalso (ty=Le orelse ty=Lt) then sys_error "multiply_ineq"
+  else if n = 0 andalso ty = Lt then raise Fail "multiply_ineq"
+  else if n < 0 andalso (ty=Le orelse ty=Lt) then raise Fail "multiply_ineq"
   else Lineq (n * k, ty, map (Integer.mult n) l, Multiplied (n, just));
 
 (* ------------------------------------------------------------------------- *)
@@ -352,7 +352,7 @@
         if (c1 >= 0) = (c2 >= 0)
         then if ty1 = Eq then (~m1,m2)
              else if ty2 = Eq then (m1,~m2)
-                  else sys_error "elim_var"
+                  else raise Fail "elim_var"
         else (m1,m2)
       val (p1,p2) = if ty1=Eq andalso ty2=Eq andalso (n1 = ~1 orelse n2 = ~1)
                     then (~n1,~n2) else (n1,n2)
@@ -497,7 +497,7 @@
               (the (try_add ([thm2] RL inj_thms) thm1)
                 handle Option =>
                   (trace_thm ctxt "" thm1; trace_thm ctxt "" thm2;
-                   sys_error "Linear arithmetic: failed to add thms"))
+                   raise Fail "Linear arithmetic: failed to add thms"))
           | SOME thm => thm)
       | SOME thm => thm);
 
@@ -598,7 +598,7 @@
                 else lineq(c,Lt,diff,just)
      | "~<"  => lineq(~c,Le,map (op~) diff,NotLessD(just))
      | "="   => lineq(c,Eq,diff,just)
-     | _     => sys_error("mklineq" ^ rel)
+     | _     => raise Fail ("mklineq" ^ rel)
   end;
 
 (* ------------------------------------------------------------------------- *)
diff -r 11846d9800de -r 665862241968 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Nov 03 10:51:40 2010 +0100
+++ b/src/Pure/Isar/code.ML	Wed Nov 03 11:06:22 2010 +0100
@@ -222,7 +222,7 @@
 
 fun invoke f k = case Datatab.lookup (! kinds) k
  of SOME kind => f kind
-  | NONE => sys_error "Invalid code data identifier";
+  | NONE => raise Fail "Invalid code data identifier";
 
 in
 
diff -r 11846d9800de -r 665862241968 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Nov 03 10:51:40 2010 +0100
+++ b/src/Pure/codegen.ML	Wed Nov 03 11:06:22 2010 +0100
@@ -354,10 +354,11 @@
 fun is_ascii_letdig x = Symbol.is_ascii_letter x orelse
   Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x;
 
-fun dest_sym s = (case split_last (snd (take_prefix (fn c => c = "\\") (explode s))) of
+fun dest_sym s =
+  (case split_last (snd (take_prefix (fn c => c = "\\") (explode s))) of
     ("<" :: "^" :: xs, ">") => (true, implode xs)
   | ("<" :: xs, ">") => (false, implode xs)
-  | _ => sys_error "dest_sym");
+  | _ => raise Fail "dest_sym");
 
 fun mk_id s = if s = "" then "" else
   let
@@ -378,7 +379,7 @@
 
 fun mk_long_id (p as (tab, used)) module s =
   let
-    fun find_name [] = sys_error "mk_long_id"
+    fun find_name [] = raise Fail "mk_long_id"
       | find_name (ys :: yss) =
           let
             val s' = Long_Name.implode ys