# HG changeset patch
# User wenzelm
# Date 1152727153 -7200
# Node ID ba1676dd35462f2fbdc279b56fcf3b697fb15fa7
# Parent  c2ffa178331983ff41f295ba7724a7c1579fb316
query/bang_colon: separate tokens;

diff -r c2ffa1783319 -r ba1676dd3546 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed Jul 12 17:40:52 2006 +0200
+++ b/src/Pure/Isar/args.ML	Wed Jul 12 19:59:13 2006 +0200
@@ -244,8 +244,8 @@
 val colon = $$$ ":";
 val query = $$$ "?";
 val bang = $$$ "!";
-val query_colon = $$$ "?:";
-val bang_colon = $$$ "!:";
+val query_colon = $$$ "?" ^^ $$$ ":";
+val bang_colon = $$$ "!" ^^ $$$ ":";
 
 fun parens scan = $$$ "(" |-- scan --| $$$ ")";
 fun bracks scan = $$$ "[" |-- scan --| $$$ "]";