src/HOL/Tools/Qelim/cooper.ML

   val notz =
     let val tab = fold Inttab.update
           (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
    Const(@{const_name HOL.conj},_)$_$_ => Conv.binop_conv unit_conv t
   | Const(@{const_name HOL.disj},_)$_$_ => Conv.binop_conv unit_conv t

            (Thm.apply (Thm.apply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
    in Thm.equal_elim (Thm.symmetric th) TrueI end;
  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)
       (Thm.apply @{cterm Trueprop}
            (Thm.apply (Thm.apply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))

                                 [eq, the (Termtab.lookup inStab (term_of s))]
                  in (term_of t, th) end)
                   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
    end
  val cpth' = Thm.transitive uth (cpth RS eq_reflection)