From 2f324fc9e868e0775e1401833b74af15652c6732 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 12 Apr 2009 14:19:15 -0400 Subject: Classes as optional arguments to Basis.tag --- src/elab_env.sml | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) (limited to 'src/elab_env.sml') diff --git a/src/elab_env.sml b/src/elab_env.sml index 6dae1d4b..62a310f2 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -899,19 +899,19 @@ fun sgnS_con (str, (sgns, strs, cons)) c = end) | _ => c -fun sgnS_con' (arg as (m1, ms', (sgns, strs, cons))) c = - case c of - CModProj (m1, ms, x) => - (case IM.find (strs, m1) of - NONE => c - | SOME m1x => CModProj (m1, ms' @ m1x :: ms, x)) - | CNamed n => - (case IM.find (cons, n) of - NONE => c - | SOME nx => CModProj (m1, ms', nx)) - | CApp (c1, c2) => CApp ((sgnS_con' arg (#1 c1), #2 c1), - (sgnS_con' arg (#1 c2), #2 c2)) - | _ => c +fun sgnS_con' (m1, ms', (sgns, strs, cons)) = + U.Con.map {kind = fn x => x, + con = fn c => + case c of + CModProj (m1, ms, x) => + (case IM.find (strs, m1) of + NONE => c + | SOME m1x => CModProj (m1, ms' @ m1x :: ms, x)) + | CNamed n => + (case IM.find (cons, n) of + NONE => c + | SOME nx => CModProj (m1, ms', nx)) + | _ => c} fun sgnS_sgn (str, (sgns, strs, cons)) sgn = case sgn of @@ -1026,7 +1026,7 @@ fun enrichClasses env classes (m1, ms) sgn = | SOME (cn, nvs, cs, c) => let val loc = #2 c - fun globalize (c, loc) = (sgnS_con' (m1, ms, fmap) c, loc) + val globalize = sgnS_con' (m1, ms, fmap) val nc = case cn of -- cgit v1.2.3