constify: qualified is const;
authorwenzelm
Fri, 10 Oct 1997 15:48:10 +0200
changeset 3830 7797327eca1d
parent 3829 d7333ef9e72c
child 3831 45e2e7ba31b8
constify: qualified is const;
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