# HG changeset patch
# User wenzelm
# Date 876491088 -7200
# Node ID c13504a27d8ef6916e96ff30bd18281f6f264bbd
# Parent  0caedb36900d83ea99c281619755c5610a275119
decode: qualified is always const;

diff -r 0caedb36900d -r c13504a27d8e src/Pure/type.ML
--- a/src/Pure/type.ML	Fri Oct 10 14:51:58 1997 +0200
+++ b/src/Pure/type.ML	Fri Oct 10 15:44:48 1997 +0200
@@ -838,7 +838,7 @@
       | decode (t $ u) = decode t $ decode u
       | decode (Free (x, T)) =
           let val c = map_const x in
-            if is_const c then Const (c, certT T)
+            if is_const c orelse NameSpace.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))
           end