diff -r 45f3c90b2d27 -r b9bbdf7eab3b src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Thu May 31 18:16:57 2007 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Thu May 31 18:16:58 2007 +0200
@@ -123,7 +123,7 @@
           (case (map_free a, map_const a) of
             (SOME x, _) => Free (x, map_type T)
           | (_, SOME c) => Const (c, map_type T)
-          | _ => Free (a, map_type T))
+          | _ => (if NameSpace.is_qualified a then Const else Free) (a, map_type T))
       | decode (Var (xi, T)) = Var (xi, map_type T)
       | decode (t as Bound _) = t;
   in decode tm end;