replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
authorwenzelm
Wed Nov 03 11:06:22 2010 +0100 (2010-11-03)
changeset 40316665862241968
parent 40315 11846d9800de
child 40317 1eac228c52b3
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
src/HOL/Library/Eval_Witness.thy
src/HOL/Tools/inductive.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/Isar/code.ML
src/Pure/codegen.ML
     1.1 --- a/src/HOL/Library/Eval_Witness.thy	Wed Nov 03 10:51:40 2010 +0100
     1.2 +++ b/src/HOL/Library/Eval_Witness.thy	Wed Nov 03 11:06:22 2010 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4    fun dest_exs  0 t = t
     1.5      | dest_exs n (Const (@{const_name Ex}, _) $ Abs (v,T,b)) = 
     1.6        Abs (v, check_type T, dest_exs (n - 1) b)
     1.7 -    | dest_exs _ _ = sys_error "dest_exs";
     1.8 +    | dest_exs _ _ = raise Fail "dest_exs";
     1.9    val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
    1.10  in
    1.11    if Code_Runtime.dynamic_value_strict (Eval_Method.get, Eval_Method.put, "Eval_Method.put") thy NONE (K I) t ws
     2.1 --- a/src/HOL/Tools/inductive.ML	Wed Nov 03 10:51:40 2010 +0100
     2.2 +++ b/src/HOL/Tools/inductive.ML	Wed Nov 03 11:06:22 2010 +0100
     2.3 @@ -229,7 +229,7 @@
     2.4  
     2.5  fun arg_types_of k c = drop k (binder_types (fastype_of c));
     2.6  
     2.7 -fun find_arg T x [] = sys_error "find_arg"
     2.8 +fun find_arg T x [] = raise Fail "find_arg"
     2.9    | find_arg T x ((p as (_, (SOME _, _))) :: ps) =
    2.10        apsnd (cons p) (find_arg T x ps)
    2.11    | find_arg T x ((p as (U, (NONE, y))) :: ps) =
     3.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Nov 03 10:51:40 2010 +0100
     3.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Nov 03 11:06:22 2010 +0100
     3.3 @@ -327,8 +327,8 @@
     3.4  
     3.5  fun multiply_ineq n (i as Lineq(k,ty,l,just)) =
     3.6    if n = 1 then i
     3.7 -  else if n = 0 andalso ty = Lt then sys_error "multiply_ineq"
     3.8 -  else if n < 0 andalso (ty=Le orelse ty=Lt) then sys_error "multiply_ineq"
     3.9 +  else if n = 0 andalso ty = Lt then raise Fail "multiply_ineq"
    3.10 +  else if n < 0 andalso (ty=Le orelse ty=Lt) then raise Fail "multiply_ineq"
    3.11    else Lineq (n * k, ty, map (Integer.mult n) l, Multiplied (n, just));
    3.12  
    3.13  (* ------------------------------------------------------------------------- *)
    3.14 @@ -352,7 +352,7 @@
    3.15          if (c1 >= 0) = (c2 >= 0)
    3.16          then if ty1 = Eq then (~m1,m2)
    3.17               else if ty2 = Eq then (m1,~m2)
    3.18 -                  else sys_error "elim_var"
    3.19 +                  else raise Fail "elim_var"
    3.20          else (m1,m2)
    3.21        val (p1,p2) = if ty1=Eq andalso ty2=Eq andalso (n1 = ~1 orelse n2 = ~1)
    3.22                      then (~n1,~n2) else (n1,n2)
    3.23 @@ -497,7 +497,7 @@
    3.24                (the (try_add ([thm2] RL inj_thms) thm1)
    3.25                  handle Option =>
    3.26                    (trace_thm ctxt "" thm1; trace_thm ctxt "" thm2;
    3.27 -                   sys_error "Linear arithmetic: failed to add thms"))
    3.28 +                   raise Fail "Linear arithmetic: failed to add thms"))
    3.29            | SOME thm => thm)
    3.30        | SOME thm => thm);
    3.31  
    3.32 @@ -598,7 +598,7 @@
    3.33                  else lineq(c,Lt,diff,just)
    3.34       | "~<"  => lineq(~c,Le,map (op~) diff,NotLessD(just))
    3.35       | "="   => lineq(c,Eq,diff,just)
    3.36 -     | _     => sys_error("mklineq" ^ rel)
    3.37 +     | _     => raise Fail ("mklineq" ^ rel)
    3.38    end;
    3.39  
    3.40  (* ------------------------------------------------------------------------- *)
     4.1 --- a/src/Pure/Isar/code.ML	Wed Nov 03 10:51:40 2010 +0100
     4.2 +++ b/src/Pure/Isar/code.ML	Wed Nov 03 11:06:22 2010 +0100
     4.3 @@ -222,7 +222,7 @@
     4.4  
     4.5  fun invoke f k = case Datatab.lookup (! kinds) k
     4.6   of SOME kind => f kind
     4.7 -  | NONE => sys_error "Invalid code data identifier";
     4.8 +  | NONE => raise Fail "Invalid code data identifier";
     4.9  
    4.10  in
    4.11  
     5.1 --- a/src/Pure/codegen.ML	Wed Nov 03 10:51:40 2010 +0100
     5.2 +++ b/src/Pure/codegen.ML	Wed Nov 03 11:06:22 2010 +0100
     5.3 @@ -354,10 +354,11 @@
     5.4  fun is_ascii_letdig x = Symbol.is_ascii_letter x orelse
     5.5    Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x;
     5.6  
     5.7 -fun dest_sym s = (case split_last (snd (take_prefix (fn c => c = "\\") (explode s))) of
     5.8 +fun dest_sym s =
     5.9 +  (case split_last (snd (take_prefix (fn c => c = "\\") (explode s))) of
    5.10      ("<" :: "^" :: xs, ">") => (true, implode xs)
    5.11    | ("<" :: xs, ">") => (false, implode xs)
    5.12 -  | _ => sys_error "dest_sym");
    5.13 +  | _ => raise Fail "dest_sym");
    5.14  
    5.15  fun mk_id s = if s = "" then "" else
    5.16    let
    5.17 @@ -378,7 +379,7 @@
    5.18  
    5.19  fun mk_long_id (p as (tab, used)) module s =
    5.20    let
    5.21 -    fun find_name [] = sys_error "mk_long_id"
    5.22 +    fun find_name [] = raise Fail "mk_long_id"
    5.23        | find_name (ys :: yss) =
    5.24            let
    5.25              val s' = Long_Name.implode ys