summaryrefslogtreecommitdiff
path: root/src/option_key_fn.sml
diff options
context:
space:
mode:
authorGravatar Ziv Scully <ziv@mit.edu>2015-07-20 23:25:44 -0700
committerGravatar Ziv Scully <ziv@mit.edu>2015-07-20 23:25:44 -0700
commit4ff7cf9503b917dcc8db1de3ba03b513240f7dc8 (patch)
tree21db757c04d6064aee147c73a73f624753871ac1 /src/option_key_fn.sml
parent0cfbe4639f076d50f2a3bbc9e6f566a452a43167 (diff)
Use uniform representation of comparisons for better simplification.
Diffstat (limited to 'src/option_key_fn.sml')
-rw-r--r--src/option_key_fn.sml3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/option_key_fn.sml b/src/option_key_fn.sml
index ba636d4e..27ba9138 100644
--- a/src/option_key_fn.sml
+++ b/src/option_key_fn.sml
@@ -1,4 +1,5 @@
-functor OptionKeyFn(K : ORD_KEY) : ORD_KEY = struct
+functor OptionKeyFn(K : ORD_KEY)
+ : ORD_KEY where type ord_key = K.ord_key option = struct
type ord_key = K.ord_key option