836 else constrain (Abs (x, certT T, decode t)) (decodeT typ --> dummyT) |
836 else constrain (Abs (x, certT T, decode t)) (decodeT typ --> dummyT) |
837 | decode (Abs (x, T, t)) = Abs (x, certT T, decode t) |
837 | decode (Abs (x, T, t)) = Abs (x, certT T, decode t) |
838 | decode (t $ u) = decode t $ decode u |
838 | decode (t $ u) = decode t $ decode u |
839 | decode (Free (x, T)) = |
839 | decode (Free (x, T)) = |
840 let val c = map_const x in |
840 let val c = map_const x in |
841 if is_const c then Const (c, certT T) |
841 if is_const c orelse NameSpace.qualified c then Const (c, certT T) |
842 else if T = dummyT then Free (x, get_type (x, ~1)) |
842 else if T = dummyT then Free (x, get_type (x, ~1)) |
843 else constrain (Free (x, certT T)) (get_type (x, ~1)) |
843 else constrain (Free (x, certT T)) (get_type (x, ~1)) |
844 end |
844 end |
845 | decode (Var (xi, T)) = |
845 | decode (Var (xi, T)) = |
846 if T = dummyT then Var (xi, get_type xi) |
846 if T = dummyT then Var (xi, get_type xi) |