prefer explicitly qualified exceptions, which is particular important for robust handlers;

--- a/src/HOL/BNF/Tools/bnf_def.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Sat May 11 16:57:18 2013 +0200
@@ -123,7 +123,7 @@
   {map_id = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
    bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, rel_OO_Grp = rel};
 
-fun dest_cons [] = raise Empty
+fun dest_cons [] = raise List.Empty
   | dest_cons (x :: xs) = (x, xs);
 
 fun mk_axioms n thms = thms

--- a/src/HOL/Matrix_LP/Cplex_tools.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Sat May 11 16:57:18 2013 +0200
@@ -973,7 +973,7 @@
     result
     end
     handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
-     | Option => raise (Load_cplexResult "Option")
+     | Option.Option => raise (Load_cplexResult "Option")
 
 fun load_cplexResult name =
     let
@@ -1122,7 +1122,7 @@
     result
     end
     handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
-     | Option => raise (Load_cplexResult "Option")
+     | Option.Option => raise (Load_cplexResult "Option")
 
 exception Execute of string;
 

--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat May 11 16:57:18 2013 +0200
@@ -194,7 +194,7 @@
              [s] => the_default (s, s) (first_field "\<emdash>" s)
            | ["", s2] => ("-" ^ s2, "-" ^ s2)
            | [s1, s2] => (s1, s2)
-           | _ => raise Option)
+           | _ => raise Option.Option)
           |> pairself (maxed_int_from_string min_int)
       in if k1 <= k2 then k1 upto k2 else k1 downto k2 end
       handle Option.Option =>

--- a/src/HOL/Tools/Qelim/cooper.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Sat May 11 16:57:18 2013 +0200
@@ -384,9 +384,9 @@
           (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
     in
       fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_number))
-        handle Option =>
+        handle Option.Option =>
           (writeln ("noz: Theorems-Table contains no entry for " ^
-              Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
+              Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option.Option)
     end
   fun unit_conv t =
    case (term_of t) of
@@ -472,9 +472,9 @@
  val dvd =
    let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
      fn ct => the (Inttab.lookup tab (term_of ct |> dest_number))
-       handle Option =>
+       handle Option.Option =>
         (writeln ("dvd: Theorems-Table contains no entry for" ^
-            Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
+            Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option.Option)
    end
  val dp =
    let val th = Simplifier.rewrite (put_simpset lin_ss ctxt)
@@ -541,9 +541,9 @@
                   sths) Termtab.empty
         in
           fn ct => the (Termtab.lookup tab (term_of ct))
-            handle Option =>
+            handle Option.Option =>
               (writeln ("inS: No theorem for " ^ Syntax.string_of_term ctxt (Thm.term_of ct));
-                raise Option)
+                raise Option.Option)
         end
        val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p
    in [dp, inf, nb, pd] MRS cpth

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Sat May 11 16:57:18 2013 +0200
@@ -41,9 +41,9 @@
 fun pop tab key =
   (let val v = hd (Inttab.lookup_list tab key) in
     (v, Inttab.remove_list (op =) (key, v) tab)
-  end) handle Empty => raise Fail "sledgehammer_compress: pop"
+  end) handle List.Empty => raise Fail "sledgehammer_compress: pop"
 fun pop_max tab = pop tab (the (Inttab.max_key tab))
-  handle Option => raise Fail "sledgehammer_compress: pop_max"
+  handle Option.Option => raise Fail "sledgehammer_compress: pop_max"
 fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
 
 (* Main function for compresing proofs *)
@@ -104,7 +104,7 @@
           | (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) =>
               cons (Term.size_of_term t, i)
           | _ => I)
-            handle Option => raise Fail "sledgehammer_compress: add_if_cand")
+            handle Option.Option => raise Fail "sledgehammer_compress: add_if_cand")
         | add_if_cand _ _ = I
       val cand_tab =
         v_fold_index (add_if_cand step_vect) refed_by_vect []
@@ -121,7 +121,7 @@
              #> handle_metis_fail
              #> Lazy.lazy)
           step_vect
-        handle Option => raise Fail "sledgehammer_compress: metis_time"
+        handle Option.Option => raise Fail "sledgehammer_compress: metis_time"
 
       fun sum_up_time lazy_time_vector =
         Vector.foldl
@@ -204,7 +204,7 @@
                           (n_metis' - 1)
             end
           end
-        handle Option => raise Fail "sledgehammer_compress: merge_steps"
+        handle Option.Option => raise Fail "sledgehammer_compress: merge_steps"
              | List.Empty => raise Fail "sledgehammer_compress: merge_steps"
     in
       merge_steps metis_time step_vect refed_by_vect cand_tab n n_metis

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat May 11 16:57:18 2013 +0200
@@ -58,11 +58,11 @@
 
 fun parse_bool_option option name s =
   (case s of
-     "smart" => if option then NONE else raise Option
+     "smart" => if option then NONE else raise Option.Option
    | "false" => SOME false
    | "true" => SOME true
    | "" => SOME true
-   | _ => raise Option)
+   | _ => raise Option.Option)
   handle Option.Option =>
          let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
            error ("Parameter " ^ quote name ^ " must be assigned " ^

--- a/src/HOL/Tools/TFL/tfl.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Sat May 11 16:57:18 2013 +0200
@@ -604,7 +604,7 @@
       val vlist = #2 (USyntax.strip_comb (USyntax.rhs body))
       val plist = ListPair.zip (vlist, xlist)
       val args = map (the o AList.lookup (op aconv) plist) qvars
-                   handle Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
+                   handle Option.Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
       fun build ex      []   = []
         | build (_$rex) (v::rst) =
            let val ex1 = Term.betapply(rex, v)

--- a/src/HOL/Tools/groebner.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/HOL/Tools/groebner.ML	Sat May 11 16:57:18 2013 +0200
@@ -864,7 +864,7 @@
   val (vars,bod) = strip_exists tm
   val cjs = striplist (dest_binary @{cterm HOL.conj}) bod
   val th1 = (the (get_first (try (isolate_variable vars)) cjs)
-             handle Option => raise CTERM ("unwind_polys_conv",[tm]))
+             handle Option.Option => raise CTERM ("unwind_polys_conv",[tm]))
   val eq = Thm.lhs_of th1
   val bod' = list_mk_binop @{cterm HOL.conj} (eq::(remove op aconvc eq cjs))
   val th2 = conj_ac_rule (mk_eq bod bod')

--- a/src/Provers/Arith/fast_lin_arith.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sat May 11 16:57:18 2013 +0200
@@ -498,7 +498,7 @@
           (case try_add ([thm1] RL inj_thms) thm2 of
             NONE =>
               (the (try_add ([thm2] RL inj_thms) thm1)
-                handle Option =>
+                handle Option.Option =>
                   (trace_thm ctxt [] thm1; trace_thm ctxt [] thm2;
                    raise Fail "Linear arithmetic: failed to add thms"))
           | SOME thm => thm)

--- a/src/Pure/General/basics.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/Pure/General/basics.ML	Sat May 11 16:57:18 2013 +0200
@@ -78,7 +78,7 @@
   | is_none NONE = true;
 
 fun the (SOME x) = x
-  | the NONE = raise Option;
+  | the NONE = raise Option.Option;
 
 fun these (SOME x) = x
   | these NONE = [];

--- a/src/Pure/type.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/Pure/type.ML	Sat May 11 16:57:18 2013 +0200
@@ -379,11 +379,11 @@
 
 fun freeze_one alist (ix, sort) =
   TFree (the (AList.lookup (op =) alist ix), sort)
-    handle Option =>
+    handle Option.Option =>
       raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
 
 fun thaw_one alist (a, sort) = TVar (the (AList.lookup (op =) alist a), sort)
-  handle Option => TFree (a, sort);
+  handle Option.Option => TFree (a, sort);
 
 in
 

--- a/src/Tools/Code/code_namespace.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/Tools/Code/code_namespace.ML	Sat May 11 16:57:18 2013 +0200
@@ -125,7 +125,7 @@
           Long_Name.append (fst (dest_name name)) (base_deresolver name)
       | deresolver module_name name =
           the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name)
-          handle Option => error ("Unknown statement name: " ^ labelled_name name);
+          handle Option.Option => error ("Unknown statement name: " ^ labelled_name name);
 
   in { deresolver = deresolver, flat_program = flat_program } end;
 

--- a/src/Tools/WWW_Find/http_util.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/Tools/WWW_Find/http_util.ML	Sat May 11 16:57:18 2013 +0200
@@ -46,7 +46,7 @@
       |> Char.chr
       |> String.str
       |> Substring.full
-      handle Option => c;
+      handle Option.Option => c;
 
     fun f (done, s) =
       let

--- a/src/Tools/WWW_Find/socket_util.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/Tools/WWW_Find/socket_util.ML	Sat May 11 16:57:18 2013 +0200
@@ -26,7 +26,7 @@
            |> NetHostDB.addr
            |> rpair port
            |> INetSock.toAddr
-           handle Option => raise Fail ("Cannot resolve hostname: " ^ host));
+           handle Option.Option => raise Fail ("Cannot resolve hostname: " ^ host));
     val _ = Socket.bind (sock, addr);
     val _ = Socket.listen (sock, 5);
   in sock end;

--- a/src/ZF/Datatype_ZF.thy	Sat May 11 16:13:08 2013 +0200
+++ b/src/ZF/Datatype_ZF.thy	Sat May 11 16:57:18 2013 +0200
@@ -81,9 +81,9 @@
        val lname = #1 (dest_Const lhead) handle TERM _ => raise Match;
        val rname = #1 (dest_Const rhead) handle TERM _ => raise Match;
        val lcon_info = the (Symtab.lookup (ConstructorsData.get thy) lname)
-         handle Option => raise Match;
+         handle Option.Option => raise Match;
        val rcon_info = the (Symtab.lookup (ConstructorsData.get thy) rname)
-         handle Option => raise Match;
+         handle Option.Option => raise Match;
        val new =
            if #big_rec_name lcon_info = #big_rec_name rcon_info
                andalso not (null (#free_iffs lcon_info)) then

--- a/src/ZF/Tools/primrec_package.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Sat May 11 16:57:18 2013 +0200
@@ -49,7 +49,7 @@
     val (cname, _) = dest_Const constr
       handle TERM _ => raise RecError "ill-formed constructor";
     val con_info = the (Symtab.lookup (ConstructorsData.get thy) cname)
-      handle Option =>
+      handle Option.Option =>
       raise RecError "cannot determine datatype associated with function"
 
     val (ls, cargs, rs) = (map dest_Free ls_frees,