src/Pure/Syntax/type_ext.ML
changeset 30364 577edc39b501
parent 29565 3f8b24fcfbd6
child 32784 1a5dde5079ac
--- a/src/Pure/Syntax/type_ext.ML	Sun Mar 08 17:19:15 2009 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Sun Mar 08 17:26:14 2009 +0100
@@ -129,7 +129,7 @@
           (case (map_free a, map_const a) of
             (SOME x, _) => Free (x, map_type T)
           | (_, (true, c)) => Const (c, map_type T)
-          | (_, (false, c)) => (if NameSpace.is_qualified c then Const else Free) (c, map_type T))
+          | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, map_type T))
       | decode (Var (xi, T)) = Var (xi, map_type T)
       | decode (t as Bound _) = t;
   in decode tm end;