summaryrefslogtreecommitdiff
path: root/src/expl_util.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-06 10:43:48 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-06 10:43:48 -0500
commitea5a24773259c147e806960843d3305a3c72067b (patch)
tree2e714f5fc0b6c669bad6c201f3a4b11fec490513 /src/expl_util.sml
parent12bb99a0ba702af12e89bfe544f2a572e5d4818d (diff)
Cookies through explify
Diffstat (limited to 'src/expl_util.sml')
-rw-r--r--src/expl_util.sml9
1 files changed, 1 insertions, 8 deletions
diff --git a/src/expl_util.sml b/src/expl_util.sml
index 337ea8d6..2bd9eabd 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -432,11 +432,6 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
S.map2 (sg ctx s,
fn s' =>
(SgiSgn (x, n, s'), loc))
- | SgiTable (tn, x, n, c) =>
- S.map2 (con ctx c,
- fn c' =>
- (SgiTable (tn, x, n, c'), loc))
- | SgiSequence _ => S.return2 siAll
and sg ctx s acc =
S.bindP (sg' ctx s acc, sgn ctx)
@@ -458,9 +453,7 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
| SgiStr (x, _, sgn) =>
bind (ctx, Str (x, sgn))
| SgiSgn (x, _, sgn) =>
- bind (ctx, Sgn (x, sgn))
- | SgiTable _ => ctx
- | SgiSequence _ => ctx,
+ bind (ctx, Sgn (x, sgn)),
sgi ctx si)) ctx sgis,
fn sgis' =>
(SgnConst sgis', loc))