1.1 --- a/src/Pure/Syntax/syntax.ML	Sat Apr 15 17:41:20 2000 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Apr 17 13:57:55 2000 +0200
     1.3 @@ -281,10 +281,11 @@
     1.4      val {lexicon, logtypes, prmodes, gram, prtabs, ...} = tabs;
     1.5      val prmodes' = sort_strings (filter_out (equal "") prmodes);
     1.6    in
     1.7 -    Pretty.writeln (pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon));
     1.8 -    Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes));
     1.9 -    Pretty.writeln (Pretty.big_list "prods:" (Parser.pretty_gram gram));
    1.10 -    Pretty.writeln (pretty_strs_qs "print modes:" prmodes')
    1.11 +    [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
    1.12 +      Pretty.strs ("logtypes:" :: logtypes),
    1.13 +      Pretty.big_list "prods:" (Parser.pretty_gram gram),
    1.14 +      pretty_strs_qs "print modes:" prmodes']
    1.15 +    |> Pretty.chunks |> Pretty.writeln
    1.16    end;
    1.17  
    1.18  
    1.19 @@ -303,14 +304,15 @@
    1.20      val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
    1.21        print_ruletab, print_ast_trtab, tokentrtab, ...} = tabs;
    1.22    in
    1.23 -    Pretty.writeln (pretty_strs_qs "consts:" consts);
    1.24 -    Pretty.writeln (pretty_trtab "parse_ast_translation:" parse_ast_trtab);
    1.25 -    Pretty.writeln (pretty_ruletab "parse_rules:" parse_ruletab);
    1.26 -    Pretty.writeln (pretty_trtab "parse_translation:" parse_trtab);
    1.27 -    Pretty.writeln (pretty_trtab "print_translation:" print_trtab);
    1.28 -    Pretty.writeln (pretty_ruletab "print_rules:" print_ruletab);
    1.29 -    Pretty.writeln (pretty_trtab "print_ast_translation:" print_ast_trtab);
    1.30 -    Pretty.writeln (Pretty.big_list "token_translation:" (map pretty_tokentr tokentrtab))
    1.31 +    [pretty_strs_qs "consts:" consts,
    1.32 +      pretty_trtab "parse_ast_translation:" parse_ast_trtab,
    1.33 +      pretty_ruletab "parse_rules:" parse_ruletab,
    1.34 +      pretty_trtab "parse_translation:" parse_trtab,
    1.35 +      pretty_trtab "print_translation:" print_trtab,
    1.36 +      pretty_ruletab "print_rules:" print_ruletab,
    1.37 +      pretty_trtab "print_ast_translation:" print_ast_trtab,
    1.38 +      Pretty.big_list "token_translation:" (map pretty_tokentr tokentrtab)]
    1.39 +    |> Pretty.chunks |> Pretty.writeln
    1.40    end;
    1.41  
    1.42  
    1.43 @@ -425,7 +427,7 @@
    1.44  
    1.45      fun constify (ast as Ast.Constant _) = ast
    1.46        | constify (ast as Ast.Variable x) =
    1.47 -          if x mem consts orelse NameSpace.qualified x then Ast.Constant x
    1.48 +          if x mem consts orelse NameSpace.is_qualified x then Ast.Constant x
    1.49            else ast
    1.50        | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
    1.51    in