# HG changeset patch
# User wenzelm
# Date 876491290 -7200
# Node ID 7797327eca1d3cd33b27b784a39c51e84d5faceb
# Parent  d7333ef9e72cbc16e53af1dc44b3714821581ce7
constify: qualified is const;

diff -r d7333ef9e72c -r 7797327eca1d src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Oct 10 15:47:41 1997 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Oct 10 15:48:10 1997 +0200
@@ -424,7 +424,8 @@
 
     fun constify (ast as Constant _) = ast
       | constify (ast as Variable x) =
-          if x mem consts then Constant x else ast
+          if x mem consts orelse NameSpace.qualified x then Constant x
+          else ast
       | constify (Appl asts) = Appl (map constify asts);
   in
     (case read_asts syn true root str of