changeset 15531 | 08c8dad8e399 |
parent 14854 | 61bdf2ae4dc5 |
child 15570 | 8d8c70b41bab |
--- a/src/Provers/splitter.ML Fri Feb 11 18:51:00 2005 +0100 +++ b/src/Provers/splitter.ML Sun Feb 13 17:15:14 2005 +0100 @@ -332,8 +332,8 @@ (case strip_comb lhs of (Const(a,aT),args) => let val info = (aT,lhs,thm,fastype_of t,length args) in case assoc(cmap,a) of - Some infos => overwrite(cmap,(a,info::infos)) - | None => (a,[info])::cmap + SOME infos => overwrite(cmap,(a,info::infos)) + | NONE => (a,[info])::cmap end | _ => split_format_err()) | _ => split_format_err())