# HG changeset patch
# User wenzelm
# Date 1152613378 -7200
# Node ID edc96f85e069b1efe5f6ce09cd93a88fbd5fa81f
# Parent  5cf221f2a55dee73920a00798a3348e4651dd0d5
tuned;

diff -r 5cf221f2a55d -r edc96f85e069 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Tue Jul 11 12:17:30 2006 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue Jul 11 12:22:58 2006 +0200
@@ -104,8 +104,8 @@
 val scan_nat = scan_digits1 >> implode;
 val scan_int = $$ "-" ^^ scan_nat || scan_nat;
 
-val scan_hex = ($$ "0") ^^ ($$ "x") ^^ (scan_hex1 >> implode);
-val scan_bin = ($$ "0") ^^ ($$ "b") ^^ (scan_bin1 >> implode);
+val scan_hex = $$ "0" ^^ $$ "x" ^^ (scan_hex1 >> implode);
+val scan_bin = $$ "0" ^^ $$ "b" ^^ (scan_bin1 >> implode);
 
 val scan_id_nat = scan_id ^^ Scan.optional ($$ "." ^^ scan_nat) "";
 val scan_var = $$ "?" ^^ scan_id_nat;