diff -r 0c64e7e07c42 -r 3a7138442fc4 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Mon Sep 30 10:44:25 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Mon Sep 30 10:46:26 2024 +0200
@@ -597,11 +597,7 @@
       | Node_Op (name, ts) :: rest => make (make_node name (make [] [] ts) :: body) stack rest
       | Tip_Op tok :: rest => make (Tip tok :: body) stack rest
       | [] => if null stack then body else raise Fail "Pending markup blocks");
-  in
-    (case make [] [] tree_ops of
-      [t] => t
-    | ts => make_node {nonterm = root, const = ""} ts)
-  end;
+  in make_node {nonterm = root, const = ""} (make [] [] tree_ops) end;
 
 fun pretty_tree (Markup (_, ts)) = maps pretty_tree ts
   | pretty_tree (Node ({const = c, ...}, ts)) =