src/HOL/Tools/meson.ML

  val prop_of = #prop o rep_thm;
 
  (*Permits forward proof from rules that discharge assumptions*)
  fun forward_res nf st =
    case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st)
-   of Some(th,_) => th
-    | None => raise THM("forward_res", 0, [st]);
+   of SOME(th,_) => th
+    | NONE => raise THM("forward_res", 0, [st]);
 
 
  (*Are any of the constants in "bs" present in the term?*)
  fun has_consts bs =
    let fun has (Const(a,_)) = a mem bs

  fun forward_res2 nf hyps st =
    case Seq.pull
          (REPEAT
           (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
           st)
-   of Some(th,_) => th
-    | None => raise THM("forward_res2", 0, [st]);
+   of SOME(th,_) => th
+    | NONE => raise THM("forward_res2", 0, [st]);
 
  (*Remove duplicates in P|Q by assuming ~P in Q
    rls (initially []) accumulates assumptions of the form P==>False*)
  fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
      handle THM _ => tryres(th,rls)