# 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