replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;

--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Nov 03 10:20:37 2010 +0100
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Nov 03 10:48:55 2010 +0100
@@ -138,7 +138,7 @@
                       else if member (op =) [Lt, Le, Eq] c then Thm.dest_arg
                       else if member (op =) [Gt, Ge] c then Thm.dest_arg1
                       else if c = NEq then (Thm.dest_arg o Thm.dest_arg)
-                      else sys_error "decomp_mpinf: Impossible case!!") fm
+                      else raise Fail "decomp_mpinf: Impossible case!!") fm
              val [mi_th, pi_th, nmi_th, npi_th, ld_th] =
                if c = Nox then map (instantiate' [] [SOME fm])
                                     [minf_P, pinf_P, nmi_P, npi_P, ld_P]

--- a/src/HOL/Matrix/Compute_Oracle/compute.ML	Wed Nov 03 10:20:37 2010 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/compute.ML	Wed Nov 03 10:48:55 2010 +0100
@@ -115,7 +115,7 @@
     fun type_of (Free (_, ty)) = ty
       | type_of (Const (_, ty)) = ty
       | type_of (Var (_, ty)) = ty
-      | type_of _ = sys_error "infer_types: type_of error"
+      | type_of _ = raise Fail "infer_types: type_of error"
 in
 fun infer_types naming encoding =
     let
@@ -132,7 +132,7 @@
                 val (adom, arange) =
                     case aty of
                         Type ("fun", [dom, range]) => (dom, range)
-                      | _ => sys_error "infer_types: function type expected"
+                      | _ => raise Fail "infer_types: function type expected"
                 val (b, bty) = infer_types level bounds (SOME adom) b
             in
                 (a $ b, arange)
@@ -143,7 +143,8 @@
             in
                 (Abs (naming level, dom, m), ty)
             end
-          | infer_types _ _ NONE (AbstractMachine.Abs m) = sys_error "infer_types: cannot infer type of abstraction"
+          | infer_types _ _ NONE (AbstractMachine.Abs m) =
+              raise Fail "infer_types: cannot infer type of abstraction"
 
         fun infer ty term =
             let

--- a/src/HOL/Tools/TFL/tfl.ML	Wed Nov 03 10:20:37 2010 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML	Wed Nov 03 10:48:55 2010 +0100
@@ -607,8 +607,7 @@
       val vlist = #2(S.strip_comb (S.rhs body))
       val plist = ListPair.zip (vlist, xlist)
       val args = map (the o AList.lookup (op aconv) plist) qvars
-                   handle Option => sys_error
-                       "TFL fault [alpha_ex_unroll]: no correspondence"
+                   handle Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
       fun build ex      []   = []
         | build (_$rex) (v::rst) =
            let val ex1 = Term.betapply(rex, v)

--- a/src/HOL/Tools/sat_solver.ML	Wed Nov 03 10:20:37 2010 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Wed Nov 03 10:48:55 2010 +0100
@@ -321,7 +321,7 @@
           []      => [xs1]
         | (0::[]) => [xs1]
         | (0::tl) => xs1 :: clauses tl
-        | _       => sys_error "this cannot happen"
+        | _       => raise Fail "SatSolver.clauses"
       end
     (* int -> PropLogic.prop_formula *)
     fun literal_from_int i =

--- a/src/ZF/Tools/numeral_syntax.ML	Wed Nov 03 10:20:37 2010 +0100
+++ b/src/ZF/Tools/numeral_syntax.ML	Wed Nov 03 10:48:55 2010 +0100
@@ -21,7 +21,7 @@
 
 fun mk_bit 0 = Syntax.const @{const_syntax "0"}
   | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax 0}
-  | mk_bit _ = sys_error "mk_bit";
+  | mk_bit _ = raise Fail "mk_bit";
 
 fun dest_bit (Const (@{const_syntax "0"}, _)) = 0
   | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax "0"}, _)) = 1