NameSpace.is_qualified;
authorwenzelm
Mon Apr 17 14:03:51 2000 +0200 (2000-04-17 ago)
changeset 8721453b493ece0a
parent 8720 840c75ab2a7f
child 8722 f745b34dcde3
NameSpace.is_qualified;
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Mon Apr 17 13:57:55 2000 +0200
     1.2 +++ b/src/Pure/type.ML	Mon Apr 17 14:03:51 2000 +0200
     1.3 @@ -865,7 +865,7 @@
     1.4        | decode (t $ u) = decode t $ decode u
     1.5        | decode (Free (x, T)) =
     1.6            let val c = map_const x in
     1.7 -            if not (is_free x) andalso (is_const c orelse NameSpace.qualified c) then
     1.8 +            if not (is_free x) andalso (is_const c orelse NameSpace.is_qualified c) then
     1.9                Const (c, certT T)
    1.10              else if T = dummyT then Free (x, get_type (x, ~1))
    1.11              else constrain (Free (x, certT T)) (get_type (x, ~1))