# HG changeset patch
# User nipkow
# Date 797592043 -7200
# Node ID 65163737728941cfebe7a6b75bb5281cd3854d87
# Parent  f2dc38ed53ac6fab0e9810490b8c8efa099dd9ca
(binder "Q" p) generates Binder("Q",p,p); it used to be Binder("Q",0,p).

diff -r f2dc38ed53ac -r 651637377289 src/Pure/Thy/thy_parse.ML
--- 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;