--- 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)) =