src/FOLP/simpdata.ML
changeset 15531 08c8dad8e399
parent 5304 c133f16febc7
child 15570 8d8c70b41bab
--- a/src/FOLP/simpdata.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/FOLP/simpdata.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -85,8 +85,8 @@
              (case head_of p of
                 Const(a,_) =>
                   (case assoc(pairs,a) of
-                     Some(rls) => flat (map atoms ([th] RL rls))
-                   | None => [th])
+                     SOME(rls) => flat (map atoms ([th] RL rls))
+                   | NONE => [th])
               | _ => [th])
          | _ => [th])
   in atoms end;