diff -r 6f43714517ee -r 08c8dad8e399 TFL/post.ML
--- 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"