src/Provers/classical.ML

--- a/src/Provers/classical.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/Provers/classical.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -224,7 +224,7 @@
   (case try (fn () =>
     rule_by_tactic (TRYALL (etac revcut_rl))
       (th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd)) () of
-    Some th' => th'
+    SOME th' => th'
   | _ => error ("Bad format for elimination rule\n" ^ string_of_thm th));