src/Provers/hypsubst.ML

--- a/src/Provers/hypsubst.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/Provers/hypsubst.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -204,8 +204,8 @@
                                    (r+1, imp_intr_tac i)
            in
                case Seq.pull(tac st) of
-                   None       => Seq.single(st)
-                 | Some(st',_) => imptac (r',hyps) st'
+                   NONE       => Seq.single(st)
+                 | SOME(st',_) => imptac (r',hyps) st'
            end handle _ => error "?? in blast_hyp_subst_tac"
   in  imptac (0, rev hyps)  end;