# HG changeset patch
# User wenzelm
# Date 1727601514 -7200
# Node ID 71ea31c8ed8552a632d9a36177bfd80f0a20cc4f
# Parent  720bc21720205d14c3c160886b9aff6effb6e999
clarified output: count Tip entries;

diff -r 720bc2172020 -r 71ea31c8ed85 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sun Sep 29 11:08:43 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Sun Sep 29 11:18:34 2024 +0200
@@ -553,7 +553,7 @@
 
 fun token_output tok (Output (n, ts)) = Output (n + 1, Tip tok :: ts);
 
-fun node_output id (Output (_, ts)) = Output (1, [Node (id, rev ts)]);
+fun node_output id (Output (n, ts)) = Output (n, [Node (id, rev ts)]);
 
 fun append_output (Output (m, ss)) (Output (n, ts)) = Output (m + n, ss @ ts);