863 else constrain (Abs (x, certT T, decode t)) (decodeT typ --> dummyT) |
863 else constrain (Abs (x, certT T, decode t)) (decodeT typ --> dummyT) |
864 | decode (Abs (x, T, t)) = Abs (x, certT T, decode t) |
864 | decode (Abs (x, T, t)) = Abs (x, certT T, decode t) |
865 | decode (t $ u) = decode t $ decode u |
865 | decode (t $ u) = decode t $ decode u |
866 | decode (Free (x, T)) = |
866 | decode (Free (x, T)) = |
867 let val c = map_const x in |
867 let val c = map_const x in |
868 if not (is_free x) andalso (is_const c orelse NameSpace.qualified c) then |
868 if not (is_free x) andalso (is_const c orelse NameSpace.is_qualified c) then |
869 Const (c, certT T) |
869 Const (c, certT T) |
870 else if T = dummyT then Free (x, get_type (x, ~1)) |
870 else if T = dummyT then Free (x, get_type (x, ~1)) |
871 else constrain (Free (x, certT T)) (get_type (x, ~1)) |
871 else constrain (Free (x, certT T)) (get_type (x, ~1)) |
872 end |
872 end |
873 | decode (Var (xi, T)) = |
873 | decode (Var (xi, T)) = |