diff -r 9b1b50514b5e -r b34c8aa657a5 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Jun 28 15:26:45 2005 +0200
+++ b/src/HOL/HOL.thy	Tue Jun 28 15:27:45 2005 +0200
@@ -33,7 +33,6 @@
   Not           :: "bool => bool"                   ("~ _" [40] 40)
   True          :: bool
   False         :: bool
-  If            :: "[bool, 'a, 'a] => 'a"           ("(if (_)/ then (_)/ else (_))" 10)
   arbitrary     :: 'a
 
   The           :: "('a => bool) => 'a"
@@ -49,6 +48,8 @@
 
 local
 
+consts
+  If            :: "[bool, 'a, 'a] => 'a"           ("(if (_)/ then (_)/ else (_))" 10)
 
 subsubsection {* Additional concrete syntax *}