src/FOLP/simpdata.ML

         (case concl_of th of
            Const("Trueprop",_) $ p =>
              (case head_of p of
                 Const(a,_) =>
                   (case 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;
 
 fun mk_rew_rules th = map mk_eq (mk_atomize mksimps_pairs th);