(binder "Q" p) generates Binder("Q",p,p); it used to be Binder("Q",0,p).

--- a/src/Pure/Thy/thy_parse.ML	Mon Apr 10 08:49:00 1995 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Tue Apr 11 11:20:43 1995 +0200
@@ -213,8 +213,10 @@
 val infxr = "infixr" $$-- !! nat >> cat "Infixr";
 
 val binder = "binder" $$--
-  !! (string -- optional ("[" $$-- nat --$$ "]") "0" -- nat)
-  >> (cat "Binder" o mk_triple1);
+  !! (string -- ( ("[" $$-- nat --$$ "]") -- nat
+                || nat >> (fn n => (n,n))
+     )          )
+  >> (cat "Binder" o mk_triple2);
 
 val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list;