aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/elab_print.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-07-31 16:28:55 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-07-31 16:28:55 -0400
commit16d3d1c3a6d1e78faab91076c20b76fdcb90edb9 (patch)
treeef54b557b346fa95b4322478bf5fbec431944f18 /src/elab_print.sml
parentd668886a45158cf3a292fdef3fa81498efd77652 (diff)
Case through explify
Diffstat (limited to 'src/elab_print.sml')
-rw-r--r--src/elab_print.sml20
1 files changed, 9 insertions, 11 deletions
diff --git a/src/elab_print.sml b/src/elab_print.sml
index d0ff8d5f..591e019b 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -220,17 +220,15 @@ fun p_pat' par env (p, _) =
| PCon (pc, SOME p) => parenIf par (box [p_patCon env pc,
space,
p_pat' true env p])
- | PRecord (xps, flex) =>
- let
- val pps = map (fn (x, p) => box [string x, space, string "=", space, p_pat env p]) xps
- in
- box [string "{",
- p_list_sep (box [string ",", space]) (fn x => x)
- (case flex of
- NONE => pps
- | SOME _ => pps @ [string "..."]),
- string "}"]
- end
+ | PRecord xps =>
+ box [string "{",
+ p_list_sep (box [string ",", space]) (fn (x, p) =>
+ box [string x,
+ space,
+ string "=",
+ space,
+ p_pat env p]) xps,
+ string "}"]
and p_pat x = p_pat' false x