src/Pure/Syntax/syntax.ML
changeset 30364 577edc39b501
parent 30189 3633f560f4c3
child 30573 49899f26fbd1
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -301,7 +301,7 @@
     1.4        lexicon =
     1.5          if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
     1.6        gram = if changed then Parser.extend_gram gram xprods else gram,
     1.7 -      consts = Library.merge (op =) (consts1, filter_out NameSpace.is_qualified consts2),
     1.8 +      consts = Library.merge (op =) (consts1, filter_out Long_Name.is_qualified consts2),
     1.9        prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
    1.10        parse_ast_trtab =
    1.11          update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
    1.12 @@ -607,7 +607,7 @@
    1.13  
    1.14      fun constify (ast as Ast.Constant _) = ast
    1.15        | constify (ast as Ast.Variable x) =
    1.16 -          if member (op =) consts x orelse NameSpace.is_qualified x then Ast.Constant x
    1.17 +          if member (op =) consts x orelse Long_Name.is_qualified x then Ast.Constant x
    1.18            else ast
    1.19        | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
    1.20