clarified signature;

--- a/src/Pure/Syntax/parser.ML	Tue Sep 24 21:41:01 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Wed Sep 25 10:38:46 2024 +0200
@@ -14,8 +14,7 @@
   datatype parsetree =
     Node of string * parsetree list |
     Tip of Lexicon.token
-  exception PARSETREE of parsetree
-  val pretty_parsetree: parsetree -> Pretty.T
+  val pretty_parsetree: parsetree -> Pretty.T list
   val parse: gram -> string -> Lexicon.token list -> parsetree list
   val branching_level: int Config.T
 end;
@@ -497,15 +496,11 @@
   Node of string * parsetree list |
   Tip of Lexicon.token;
 
-exception PARSETREE of parsetree;
-
-fun pretty_parsetree parsetree =
-  let
-    fun pretty (Node (c, pts)) =
-          [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty pts))]
-      | pretty (Tip tok) =
-          if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else [];
-  in (case pretty parsetree of [prt] => prt | _ => raise PARSETREE parsetree) end;
+fun pretty_parsetree (Node (c, pts)) =
+      [Pretty.enclose "(" ")"
+        (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty_parsetree pts))]
+  | pretty_parsetree (Tip tok) =
+      if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else [];
 
 
 (* parser state *)

--- a/src/Pure/Syntax/syntax_phases.ML	Tue Sep 24 21:41:01 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Sep 25 10:38:46 2024 +0200
@@ -358,8 +358,7 @@
           (("Ambiguous input" ^ Position.here (Position.no_range_position pos) ^
             " produces " ^ string_of_int len ^ " parse trees" ^
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-            map (Pretty.string_of o Pretty.item o single o Parser.pretty_parsetree)
-              (take limit pts))];
+            map (Pretty.string_of o Pretty.item o Parser.pretty_parsetree) (take limit pts))];
 
   in (ambig_msgs, map (parsetree_to_ast ctxt ast_tr) pts) end;