# HG changeset patch
# User wenzelm
# Date 955973031 -7200
# Node ID 453b493ece0a3bb221b9c308b16e9f8f9fbb490c
# Parent  840c75ab2a7f5dafae9c2086205a8de89601c1ed
NameSpace.is_qualified;

diff -r 840c75ab2a7f -r 453b493ece0a src/Pure/type.ML
--- 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))