1.1 --- a/src/Pure/Syntax/syntax.ML	Fri May 21 21:46:25 2004 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Fri May 21 21:47:07 2004 +0200
     1.3 @@ -339,9 +339,9 @@
     1.4  
     1.5      fun show_pt pt =
     1.6        let
     1.7 -        val raw_ast = SynTrans.pt_to_ast (K None) pt;
     1.8 +        val [raw_ast] = SynTrans.pts_to_asts (K None) [pt];
     1.9          val _ = writeln ("raw: " ^ Ast.str_of_ast raw_ast);
    1.10 -        val pre_ast = SynTrans.pt_to_ast (lookup_tr parse_ast_trtab) pt;
    1.11 +        val [pre_ast] = SynTrans.pts_to_asts (lookup_tr parse_ast_trtab) [pt];
    1.12          val _ = Ast.normalize true true (lookup_ruletab parse_ruletab) pre_ast;
    1.13        in () end;
    1.14    in seq show_pt (Parser.parse gram root toks) end;
    1.15 @@ -359,7 +359,7 @@
    1.16      val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
    1.17  
    1.18      fun show_pt pt =
    1.19 -      warning (Pretty.string_of (Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt)));
    1.20 +      warning (Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts (K None) [pt]))));
    1.21    in
    1.22      if length pts > ! ambiguity_level then
    1.23          if ! ambiguity_is_error then
    1.24 @@ -369,7 +369,7 @@
    1.25               warning "produces the following parse trees:";
    1.26               seq show_pt pts)
    1.27      else ();
    1.28 -    map (SynTrans.pt_to_ast (lookup_tr parse_ast_trtab)) pts
    1.29 +    SynTrans.pts_to_asts (lookup_tr parse_ast_trtab) pts
    1.30    end;
    1.31  
    1.32  
    1.33 @@ -380,7 +380,7 @@
    1.34      val {parse_ruletab, parse_trtab, ...} = tabs;
    1.35      val asts = read_asts syn false (SynExt.typ_to_nonterm ty) str;
    1.36    in
    1.37 -    map (SynTrans.ast_to_term (lookup_tr parse_trtab))
    1.38 +    SynTrans.asts_to_terms (lookup_tr parse_trtab)
    1.39        (map (Ast.normalize_ast (lookup_ruletab parse_ruletab)) asts)
    1.40    end;
    1.41