src/ZF/Datatype.ML

        val (lhead, largs) = strip_comb lhs
        and (rhead, rargs) = strip_comb rhs
        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_sg sg, lname))
-         handle Library.OPTION => raise Match;
+         handle Option => raise Match;
        val rcon_info = the (Symtab.lookup (ConstructorsData.get_sg sg, rname))
-         handle Library.OPTION => raise Match;
+         handle Option => raise Match;
        val new = 
            if #big_rec_name lcon_info = #big_rec_name rcon_info 
                andalso not (null (#free_iffs lcon_info)) then
                if lname = rname then mk_new (largs, rargs)
                else Const("False",FOLogic.oT)

        val thm = Tactic.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
            simp_tac (datatype_ss addsimps #free_iffs lcon_info) 1)
          handle ERROR_MESSAGE msg =>
          (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
           raise Match)
-   in Some thm end
-   handle Match => None;
+   in SOME thm end
+   handle Match => NONE;
 
 
  val conv = 
      Simplifier.simproc (Theory.sign_of (theory "ZF")) "data_free" 
                         ["(x::i) = y"] proc;