src/HOL/HOL.thy
changeset 36363 ebaa558fc698
parent 36297 6b2b9516a3cd
child 36365 18bf20d0c2df
--- 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)