Constant "If" is now local

--- 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 *}
 

--- a/src/HOL/Import/HOL/bool.imp	Tue Jun 28 15:26:45 2005 +0200
+++ b/src/HOL/Import/HOL/bool.imp	Tue Jun 28 15:27:45 2005 +0200
@@ -26,7 +26,7 @@
   "LET" > "HOL4Compat.LET"
   "IN" > "HOL4Base.bool.IN"
   "F" > "False"
-  "COND" > "If"
+  "COND" > "HOL.If"
   "ARB" > "HOL4Base.bool.ARB"
   "?!" > "Ex1"
   "?" > "Ex"

--- a/src/HOL/Main.thy	Tue Jun 28 15:26:45 2005 +0200
+++ b/src/HOL/Main.thy	Tue Jun 28 15:27:45 2005 +0200
@@ -26,7 +26,7 @@
   "Not"     ("not")
   "op |"    ("(_ orelse/ _)")
   "op &"    ("(_ andalso/ _)")
-  "If"      ("(if _/ then _/ else _)")
+  "HOL.If"      ("(if _/ then _/ else _)")
 
   "wfrec"   ("wf'_rec?")
 

--- a/src/HOL/Modelcheck/mucke_oracle.ML	Tue Jun 28 15:26:45 2005 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Tue Jun 28 15:27:45 2005 +0200
@@ -41,7 +41,7 @@
 local
   (* searching an if-term as below as possible *)
   fun contains_if (Abs(a,T,t)) = [] |
-  contains_if (Const("If",T) $ b $ a1 $ a2) =
+  contains_if (Const("HOL.If",T) $ b $ a1 $ a2) =
   let
   fun tn (Type(s,_)) = s |
   tn _ = error "cannot master type variables in if term";
@@ -60,7 +60,7 @@
   find_replace_term t = (t,[]);
 
   fun if_substi (Abs(a,T,t)) trm = Abs(a,T,t) |
-  if_substi (Const("If",T) $ b $ a1 $ a2) t = t |
+  if_substi (Const("HOL.If",T) $ b $ a1 $ a2) t = t |
   if_substi (a $ b) t = if ((contains_if b)=[]) then ((if_substi a t)$b)
 		        else (a$(if_substi b t)) |
   if_substi t v = t;
@@ -654,7 +654,7 @@
   val tty = type_of_term t;
   val con_term = con_term_of con a;
  in
-	(Const("If",Type("fun",[Type("bool",[]),
+	(Const("HOL.If",Type("fun",[Type("bool",[]),
         Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])])) $
 	(Const("op =",Type("fun",[tty,Type("fun",[tty,Type("bool",[])])])) $
         t $ con_term) $
@@ -757,7 +757,7 @@
  fun casc_if2 sg tl x con [] ty trm [] = trm | (* should never occur *)
  casc_if2 sg tl x con [arg] ty trm [] = x_subst sg tl x (con_term_of con arg) trm |
  casc_if2 sg tl x con (a::r) ty trm cl =
-        Const("If",Type("fun",[Type("bool",[]),
+        Const("HOL.If",Type("fun",[Type("bool",[]),
         Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])
         ])) $
      (Const("op =",Type("fun",[ty,Type("fun",[ty,Type("bool",[])])])) $

--- a/src/HOL/eqrule_HOL_data.ML	Tue Jun 28 15:26:45 2005 +0200
+++ b/src/HOL/eqrule_HOL_data.ML	Tue Jun 28 15:27:45 2005 +0200
@@ -33,7 +33,7 @@
 val tranformation_pairs =
   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    ("All", [spec]), ("True", []), ("False", []),
-   ("If", [if_bool_eq_conj RS iffD1])];
+   ("HOL.If", [if_bool_eq_conj RS iffD1])];
 
 (*
 val mk_atomize:      (string * thm list) list -> thm -> thm list

--- a/src/HOL/simpdata.ML	Tue Jun 28 15:26:45 2005 +0200
+++ b/src/HOL/simpdata.ML	Tue Jun 28 15:27:45 2005 +0200
@@ -240,7 +240,7 @@
 val mksimps_pairs =
   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    ("All", [spec]), ("True", []), ("False", []),
-   ("If", [if_bool_eq_conj RS iffD1])];
+   ("HOL.If", [if_bool_eq_conj RS iffD1])];
 
 (*
 val mk_atomize:      (string * thm list) list -> thm -> thm list