changeset 15531 | 08c8dad8e399 |
parent 15481 | fc075ae929e4 |
child 15662 | 7e3bee7df06e |
--- 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;