author | wenzelm |
Mon, 17 Apr 2000 14:03:51 +0200 | |
changeset 8721 | 453b493ece0a |
parent 8720 | 840c75ab2a7f |
child 8722 | f745b34dcde3 |
src/Pure/type.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/type.ML Mon Apr 17 13:57:55 2000 +0200 +++ b/src/Pure/type.ML Mon Apr 17 14:03:51 2000 +0200 @@ -865,7 +865,7 @@ | decode (t $ u) = decode t $ decode u | decode (Free (x, T)) = let val c = map_const x in - if not (is_free x) andalso (is_const c orelse NameSpace.qualified c) then + if not (is_free x) andalso (is_const c orelse NameSpace.is_qualified c) then Const (c, certT T) else if T = dummyT then Free (x, get_type (x, ~1)) else constrain (Free (x, certT T)) (get_type (x, ~1))