diff -r 6f43714517ee -r 08c8dad8e399 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/HOL/Tools/meson.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -44,8 +44,8 @@
  (*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?*)
@@ -126,8 +126,8 @@
          (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*)