# HG changeset patch
# User wenzelm
# Date 902761300 -7200
# Node ID 0c055426fd6bd701fa601b15da71d5278b9fb8c3
# Parent  cfb74a99182c87628356bd36fec4b50c8675d74c
??id syntax for text variables;

diff -r cfb74a99182c -r 0c055426fd6b src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Mon Aug 10 17:01:02 1998 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Mon Aug 10 17:01:40 1998 +0200
@@ -200,7 +200,8 @@
   ("_K",           "_",                             NoSyn),
   ("",             "id => logic",                   Delimfix "_"),
   ("",             "longid => logic",               Delimfix "_"),
-  ("",             "var => logic",                  Delimfix "_")];
+  ("",             "var => logic",                  Delimfix "_"),
+  ("_BIND",        "id => logic",                   Delimfix "??_")];
 
 val pure_appl_syntax =
  [("_appl", "[('b => 'a), args] => logic", Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri)),