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

--- a/src/HOL/Tools/Function/context_tree.ML	Wed Nov 03 11:06:22 2010 +0100
+++ b/src/HOL/Tools/Function/context_tree.ML	Wed Nov 03 11:11:49 2010 +0100
@@ -125,7 +125,7 @@
      (cterm_instantiate inst r, dep, branches)
    end
    handle Pattern.MATCH => find_cong_rule ctx fvar h rs t)
-  | find_cong_rule _ _ _ [] _ = sys_error "Function/context_tree.ML: No cong rule found!"
+  | find_cong_rule _ _ _ [] _ = raise General.Fail "No cong rule found!"
 
 
 fun mk_tree fvar h ctxt t =

--- a/src/HOL/Tools/Function/lexicographic_order.ML	Wed Nov 03 11:06:22 2010 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Wed Nov 03 11:11:49 2010 +0100
@@ -117,7 +117,7 @@
        rtac @{thm "mlex_leq"} 1
        THEN PRIMITIVE (Thm.elim_implies thm)
        THEN prove_row cs
-   | _ => sys_error "lexicographic_order")
+   | _ => raise General.Fail "lexicographic_order")
  | prove_row [] = no_tac;
 
 

--- a/src/HOL/Tools/Function/mutual.ML	Wed Nov 03 11:06:22 2010 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Wed Nov 03 11:11:49 2010 +0100
@@ -185,7 +185,7 @@
       case cprems_of psimp of
         [] => (psimp, I)
       | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
-      | _ => sys_error "Too many conditions"
+      | _ => raise General.Fail "Too many conditions"
 
   in
     Goal.prove ctxt [] []

--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Nov 03 11:06:22 2010 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Nov 03 11:11:49 2010 +0100
@@ -171,8 +171,8 @@
           else (thm COMP (Thm.lift_rule (cprop_of thm) @{thm less_imp_le}))
         | SOME (Termination.LessEq (thm, _))  =>
           if not bStrict then thm
-          else sys_error "get_desc_thm"
-        | _ => sys_error "get_desc_thm"
+          else raise Fail "get_desc_thm"
+        | _ => raise Fail "get_desc_thm"
 
     val (label, lev, sl, covering) = certificate