# HG changeset patch
# User huffman
# Date 1272299191 25200
# Node ID ebaa558fc69822f97ae98eaceb770644f712178f
# Parent  06475a1547cbb1ac1386ac65199978dc6b37e5ce
syntax precedence for If and Let

diff -r 06475a1547cb -r ebaa558fc698 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Apr 26 09:21:25 2010 -0700
+++ b/src/HOL/HOL.thy	Mon Apr 26 09:26:31 2010 -0700
@@ -73,7 +73,7 @@
 local
 
 consts
-  If            :: "[bool, 'a, 'a] => 'a"           ("(if (_)/ then (_)/ else (_))" 10)
+  If            :: "[bool, 'a, 'a] => 'a"           ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)
 
 
 subsubsection {* Additional concrete syntax *}
@@ -118,7 +118,7 @@
   "_bind"       :: "[pttrn, 'a] => letbind"              ("(2_ =/ _)" 10)
   ""            :: "letbind => letbinds"                 ("_")
   "_binds"      :: "[letbind, letbinds] => letbinds"     ("_;/ _")
-  "_Let"        :: "[letbinds, 'a] => 'a"                ("(let (_)/ in (_))" 10)
+  "_Let"        :: "[letbinds, 'a] => 'a"                ("(let (_)/ in (_))" [0, 10] 10)
 
   "_case_syntax":: "['a, cases_syn] => 'b"               ("(case _ of/ _)" 10)
   "_case1"      :: "['a, 'b] => case_syn"                ("(2_ =>/ _)" 10)