clarified output: count Tip entries;
authorwenzelm
Sun, 29 Sep 2024 11:18:34 +0200
changeset 80995 71ea31c8ed85
parent 80994 720bc2172020
child 80996 c35d7bddbb00
clarified output: count Tip entries;
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);