# HG changeset patch
# User wenzelm
# Date 1288796175 -3600
# Node ID 07264bbb5f30c6130afa8d8dc1f9999df89c137d
# Parent  3b7f570723f9908e5b29662b04c508359817bd66# Parent  daaa0b236a3f1715277c60c06bfa9180eea1fe48
merged

diff -r 3b7f570723f9 -r 07264bbb5f30 NEWS
--- a/NEWS	Wed Nov 03 07:02:09 2010 -0700
+++ b/NEWS	Wed Nov 03 15:56:15 2010 +0100
@@ -349,6 +349,10 @@
 
 *** ML ***
 
+* Discontinued obsolete function sys_error and exception SYS_ERROR.
+See implementation manual for further details on exceptions in
+Isabelle/ML.
+
 * Antiquotation @{assert} inlines a function bool -> unit that raises
 Fail if the argument is false.  Due to inlining the source position of
 failed assertions is included in the error output.
diff -r 3b7f570723f9 -r 07264bbb5f30 src/HOL/Decision_Procs/ferrante_rackoff.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Nov 03 15:56:15 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]
diff -r 3b7f570723f9 -r 07264bbb5f30 src/HOL/Library/Eval_Witness.thy
--- a/src/HOL/Library/Eval_Witness.thy	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Library/Eval_Witness.thy	Wed Nov 03 15:56:15 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 3b7f570723f9 -r 07264bbb5f30 src/HOL/Matrix/Compute_Oracle/compute.ML
--- a/src/HOL/Matrix/Compute_Oracle/compute.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Matrix/Compute_Oracle/compute.ML	Wed Nov 03 15:56:15 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
diff -r 3b7f570723f9 -r 07264bbb5f30 src/HOL/Tools/Function/context_tree.ML
--- a/src/HOL/Tools/Function/context_tree.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/Function/context_tree.ML	Wed Nov 03 15:56:15 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 =
diff -r 3b7f570723f9 -r 07264bbb5f30 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Wed Nov 03 15:56:15 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;
 
 
diff -r 3b7f570723f9 -r 07264bbb5f30 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/Function/mutual.ML	Wed Nov 03 15:56:15 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 [] []
diff -r 3b7f570723f9 -r 07264bbb5f30 src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Nov 03 15:56:15 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
 
diff -r 3b7f570723f9 -r 07264bbb5f30 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/TFL/tfl.ML	Wed Nov 03 15:56:15 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)
diff -r 3b7f570723f9 -r 07264bbb5f30 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/inductive.ML	Wed Nov 03 15:56:15 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 3b7f570723f9 -r 07264bbb5f30 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/record.ML	Wed Nov 03 15:56:15 2010 +0100
@@ -1578,7 +1578,7 @@
           (case rev params of
             [] =>
               (case AList.lookup (op =) (Term.add_frees g []) s of
-                NONE => sys_error "try_param_tac: no such variable"
+                NONE => error "try_param_tac: no such variable"
               | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
           | (_, T) :: _ =>
               [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
diff -r 3b7f570723f9 -r 07264bbb5f30 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/sat_solver.ML	Wed Nov 03 15:56:15 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 =
diff -r 3b7f570723f9 -r 07264bbb5f30 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Nov 03 15:56:15 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 3b7f570723f9 -r 07264bbb5f30 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/Pure/Isar/code.ML	Wed Nov 03 15:56:15 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 3b7f570723f9 -r 07264bbb5f30 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/Pure/Isar/runtime.ML	Wed Nov 03 15:56:15 2010 +0100
@@ -68,7 +68,6 @@
         | TERMINATE => ["Exit"]
         | TimeLimit.TimeOut => ["Timeout"]
         | TOPLEVEL_ERROR => ["Error"]
-        | SYS_ERROR msg => ["## SYSTEM ERROR ##\n" ^ msg]
         | ERROR msg => [msg]
         | Fail msg => [raised exn "Fail" [msg]]
         | THEORY (msg, thys) =>
diff -r 3b7f570723f9 -r 07264bbb5f30 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/Pure/ML/ml_lex.ML	Wed Nov 03 15:56:15 2010 +0100
@@ -73,7 +73,14 @@
 fun check_content_of tok =
   (case kind_of tok of
     Error msg => error msg
-  | _ => content_of tok);
+  | _ =>
+      (case tok of
+        Token (_, (Keyword, ":>")) =>
+          warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\
+            \prefer non-opaque matching (:) possibly with abstype" ^
+            Position.str_of (pos_of tok))
+      | _ => ();
+      content_of tok));
 
 val flatten = implode o map (Symbol.escape o check_content_of);
 
diff -r 3b7f570723f9 -r 07264bbb5f30 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/Pure/codegen.ML	Wed Nov 03 15:56:15 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
diff -r 3b7f570723f9 -r 07264bbb5f30 src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/Pure/library.ML	Wed Nov 03 15:56:15 2010 +0100
@@ -29,8 +29,6 @@
   val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a
 
   (*errors*)
-  exception SYS_ERROR of string
-  val sys_error: string -> 'a
   exception ERROR of string
   val error: string -> 'a
   val cat_error: string -> string -> 'a
@@ -256,11 +254,9 @@
 fun funpow_yield (0 : int) _ x = ([], x)
   | funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
 
+
 (* errors *)
 
-exception SYS_ERROR of string;
-fun sys_error msg = raise SYS_ERROR msg;
-
 exception ERROR of string;
 fun error msg = raise ERROR msg;
 
diff -r 3b7f570723f9 -r 07264bbb5f30 src/ZF/Tools/numeral_syntax.ML
--- a/src/ZF/Tools/numeral_syntax.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/ZF/Tools/numeral_syntax.ML	Wed Nov 03 15:56:15 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
diff -r 3b7f570723f9 -r 07264bbb5f30 src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/ZF/int_arith.ML	Wed Nov 03 15:56:15 2010 +0100
@@ -4,18 +4,25 @@
 Simprocs for linear arithmetic.
 *)
 
-structure Int_Numeral_Simprocs =
+signature INT_NUMERAL_SIMPROCS =
+sig
+  val cancel_numerals: simproc list
+  val combine_numerals: simproc
+  val combine_numerals_prod: simproc
+end
+
+structure Int_Numeral_Simprocs: INT_NUMERAL_SIMPROCS =
 struct
 
 (* abstract syntax operations *)
 
 fun mk_bit 0 = @{term "0"}
   | mk_bit 1 = @{term "succ(0)"}
-  | mk_bit _ = sys_error "mk_bit";
+  | mk_bit _ = raise TERM ("mk_bit", []);
 
 fun dest_bit @{term "0"} = 0
   | dest_bit @{term "succ(0)"} = 1
-  | dest_bit _ = raise Match;
+  | dest_bit t = raise TERM ("dest_bit", [t]);
 
 fun mk_bin i =
   let
@@ -29,7 +36,7 @@
     fun bin_of @{term Pls} = []
       | bin_of @{term Min} = [~1]
       | bin_of (@{term Bit} $ bs $ b) = dest_bit b :: bin_of bs
-      | bin_of _ = sys_error "dest_bin";
+      | bin_of _ = raise TERM ("dest_bin", [tm]);
   in Numeral_Syntax.dest_binary (bin_of tm) end;
 
 
@@ -37,10 +44,8 @@
 
 fun mk_numeral i = @{const integ_of} $ mk_bin i;
 
-(*Decodes a binary INTEGER*)
-fun dest_numeral (Const(@{const_name integ_of}, _) $ w) =
-     (dest_bin w handle SYS_ERROR _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
-  | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
+fun dest_numeral (Const(@{const_name integ_of}, _) $ w) = dest_bin w
+  | dest_numeral t = raise TERM ("dest_numeral", [t]);
 
 fun find_first_numeral past (t::terms) =
         ((dest_numeral t, rev past @ terms)
@@ -59,8 +64,6 @@
 fun long_mk_sum []        = zero
   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
 
-val dest_plus = FOLogic.dest_bin @{const_name "zadd"} @{typ i};
-
 (*decompose additions AND subtractions as a sum*)
 fun dest_summing (pos, Const (@{const_name "zadd"}, _) $ t $ u, ts) =
         dest_summing (pos, t, dest_summing (pos, u, ts))
@@ -71,9 +74,6 @@
 
 fun dest_sum t = dest_summing (true, t, []);
 
-val mk_diff = FOLogic.mk_binop @{const_name "zdiff"};
-val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} @{typ i};
-
 val one = mk_numeral 1;
 val mk_times = FOLogic.mk_binop @{const_name "zmult"};