constify: qualified is const;
authorwenzelm
Fri Oct 10 15:48:10 1997 +0200 (1997-10-10)
changeset 38307797327eca1d
parent 3829 d7333ef9e72c
child 3831 45e2e7ba31b8
constify: qualified is const;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Fri Oct 10 15:47:41 1997 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Oct 10 15:48:10 1997 +0200
     1.3 @@ -424,7 +424,8 @@
     1.4  
     1.5      fun constify (ast as Constant _) = ast
     1.6        | constify (ast as Variable x) =
     1.7 -          if x mem consts then Constant x else ast
     1.8 +          if x mem consts orelse NameSpace.qualified x then Constant x
     1.9 +          else ast
    1.10        | constify (Appl asts) = Appl (map constify asts);
    1.11    in
    1.12      (case read_asts syn true root str of