changeset 15531 | 08c8dad8e399 |
parent 15171 | e0cd537c4325 |
child 15570 | 8d8c70b41bab |
--- a/TFL/post.ML Fri Feb 11 18:51:00 2005 +0100 +++ b/TFL/post.ML Sun Feb 13 17:15:14 2005 +0100 @@ -207,7 +207,7 @@ -- Lucas Dixon, Aug 2004 *) local fun get_related_thms i = - mapfilter ((fn (r,x) => if x = i then Some r else None)); + mapfilter ((fn (r,x) => if x = i then SOME r else NONE)); fun solve_eq (th, [], i) = raise ERROR_MESSAGE "derive_init_eqs: missing rules"