clarified exception -- actually reject denominator = 0;

--- a/src/HOL/Tools/lin_arith.ML	Wed Jun 01 16:02:02 2016 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Wed Jun 01 17:46:12 2016 +0200
@@ -156,7 +156,7 @@
          if we choose to do so here, the simpset used by arith must be able to
          perform the same simplifications. *)
       (* quotient 's / t', where the denominator t can be NONE *)
-      (* Note: will raise Rat.DIVZERO iff m' is @0 *)
+      (* Note: will raise Div iff m' is @0 *)
       if of_field_sort thy (domain_type T) then
         let
           val (os',m') = demult (s, m);
@@ -235,7 +235,7 @@
   | @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j)
   | @{const_name HOL.eq}            => SOME (p, i, "=", q, j)
   | _                   => NONE
-end handle Rat.DIVZERO => NONE;
+end handle General.Div => NONE;
 
 fun of_lin_arith_sort thy U =
   Sign.of_sort thy (U, @{sort Rings.linordered_idom});

--- a/src/Pure/General/rat.ML	Wed Jun 01 16:02:02 2016 +0200
+++ b/src/Pure/General/rat.ML	Wed Jun 01 17:46:12 2016 +0200
@@ -8,7 +8,6 @@
 signature RAT =
 sig
   eqtype rat
-  exception DIVZERO
   val of_int: int -> rat
   val make: int * int -> rat
   val dest: rat -> int * int
@@ -37,13 +36,12 @@
   let val m = PolyML.IntInf.lcm (q1, q2)
   in ((p1 * (m div q1), p2 * (m div q2)), m) end;
 
-exception DIVZERO;
-
-fun make (p, q) =
-  let
-    val m = PolyML.IntInf.gcd (p, q);
-    val (p', q') = (p div m, q div m) handle Div => raise DIVZERO;
-  in Rat (if q' < 0 then (~ p', ~ q') else (p', q')) end
+fun make (p, 0) = raise Div
+  | make (p, q) =
+    let
+      val m = PolyML.IntInf.gcd (p, q);
+      val (p', q') = (p div m, q div m);
+    in Rat (if q' < 0 then (~ p', ~ q') else (p', q')) end
 
 fun dest (Rat r) = r;
 
@@ -86,7 +84,7 @@
 fun inv (Rat (p, q)) =
   (case Integer.sign p of
     LESS => Rat (~ q, ~ p)
-  | EQUAL => raise DIVZERO
+  | EQUAL => raise Div
   | GREATER => Rat (q, p));
 
 fun floor (Rat (p, q)) = p div q;