src/FOL/eqrule_FOL_data.ML

 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
 structure ZF_EqRuleData : EQRULE_DATA =
 struct
 
 fun mk_eq th = case concl_of th of
-        Const("==",_)$_$_       => Some (th)
-    |   _$(Const("op <->",_)$_$_) => Some (th RS iff_reflection)
-    |   _$(Const("op =",_)$_$_) => Some (th RS eq_reflection)
-    |   _ => None;
+        Const("==",_)$_$_       => SOME (th)
+    |   _$(Const("op <->",_)$_$_) => SOME (th RS iff_reflection)
+    |   _$(Const("op =",_)$_$_) => SOME (th RS eq_reflection)
+    |   _ => NONE;
 
 val tranformation_pairs =
   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    ("All", [spec]), ("True", []), ("False", [])];
 

         (case Thm.concl_of th of
            Const("Trueprop",_) $ p =>
              (case Term.head_of p of
                 Const(a,_) =>
                   (case Library.assoc(pairs,a) of
-                     Some(rls) => flat (map atoms ([th] RL rls))
-                   | None => [th])
+                     SOME(rls) => flat (map atoms ([th] RL rls))
+                   | NONE => [th])
               | _ => [th])
          | _ => [th])
   in atoms end;
 
 val prep_meta_eq =