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

     2.1 --- a/src/HOL/Matrix/Compute_Oracle/compute.ML	Wed Nov 03 10:20:37 2010 +0100
     2.2 +++ b/src/HOL/Matrix/Compute_Oracle/compute.ML	Wed Nov 03 10:48:55 2010 +0100
     2.3 @@ -115,7 +115,7 @@
     2.4      fun type_of (Free (_, ty)) = ty
     2.5        | type_of (Const (_, ty)) = ty
     2.6        | type_of (Var (_, ty)) = ty
     2.7 -      | type_of _ = sys_error "infer_types: type_of error"
     2.8 +      | type_of _ = raise Fail "infer_types: type_of error"
     2.9  in
    2.10  fun infer_types naming encoding =
    2.11      let
    2.12 @@ -132,7 +132,7 @@
    2.13                  val (adom, arange) =
    2.14                      case aty of
    2.15                          Type ("fun", [dom, range]) => (dom, range)
    2.16 -                      | _ => sys_error "infer_types: function type expected"
    2.17 +                      | _ => raise Fail "infer_types: function type expected"
    2.18                  val (b, bty) = infer_types level bounds (SOME adom) b
    2.19              in
    2.20                  (a $ b, arange)
    2.21 @@ -143,7 +143,8 @@
    2.22              in
    2.23                  (Abs (naming level, dom, m), ty)
    2.24              end
    2.25 -          | infer_types _ _ NONE (AbstractMachine.Abs m) = sys_error "infer_types: cannot infer type of abstraction"
    2.26 +          | infer_types _ _ NONE (AbstractMachine.Abs m) =
    2.27 +              raise Fail "infer_types: cannot infer type of abstraction"
    2.28  
    2.29          fun infer ty term =
    2.30              let

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

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

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