# HG changeset patch
# User haftmann
# Date 1282899406 -7200
# Node ID 848be46708dc2e5a0f519f8f6801c57bbf6a0838
# Parent  2d638e963357cd6fcb84cca722a5dedf78582465
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj

diff -r 2d638e963357 -r 848be46708dc NEWS
--- a/NEWS	Fri Aug 27 10:55:20 2010 +0200
+++ b/NEWS	Fri Aug 27 10:56:46 2010 +0200
@@ -104,6 +104,8 @@
     Trueprop ~> HOL.Trueprop
     True ~> HOL.True
     False ~> HOL.False
+    op & ~> HOL.conj
+    op | ~> HOL.disj
     op --> ~> HOL.implies
     Not ~> HOL.Not
     The ~> HOL.The
diff -r 2d638e963357 -r 848be46708dc src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Fri Aug 27 10:56:46 2010 +0200
@@ -197,6 +197,7 @@
 apply (erule yahalom.induct,
        drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast)
 apply (simp only: Says_Server_not_range analz_image_freshK_simps)
+apply safe
 done
 
 lemma analz_insert_freshK:
diff -r 2d638e963357 -r 848be46708dc src/HOL/Boogie/Tools/boogie_tactics.ML
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -50,11 +50,11 @@
 
 
 local
-  fun explode_conj (@{term "op &"} $ t $ u) = explode_conj t @ explode_conj u
+  fun explode_conj (@{term HOL.conj} $ t $ u) = explode_conj t @ explode_conj u
     | explode_conj t = [t] 
 
   fun splt (ts, @{term HOL.implies} $ t $ u) = splt (ts @ explode_conj t, u)
-    | splt (ts, @{term "op &"} $ t $ u) = splt (ts, t) @ splt (ts, u)
+    | splt (ts, @{term HOL.conj} $ t $ u) = splt (ts, t) @ splt (ts, u)
     | splt (ts, @{term assert_at} $ _ $ t) = [(ts, t)]
     | splt (_, @{term True}) = []
     | splt tp = [tp]
diff -r 2d638e963357 -r 848be46708dc src/HOL/Boogie/Tools/boogie_vcs.ML
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -62,9 +62,9 @@
       | vc_of (@{term HOL.implies} $ @{term True} $ u) = vc_of u
       | vc_of (@{term HOL.implies} $ t $ u) =
           vc_of u |> Option.map (assume t)
-      | vc_of (@{term "op &"} $ (@{term assert_at} $ Free (n, _) $ t) $ u) =
+      | vc_of (@{term HOL.conj} $ (@{term assert_at} $ Free (n, _) $ t) $ u) =
           SOME (vc_of u |> the_default True |> assert (n, t))
-      | vc_of (@{term "op &"} $ t $ u) =
+      | vc_of (@{term HOL.conj} $ t $ u) =
           (case (vc_of t, vc_of u) of
             (NONE, r) => r
           | (l, NONE) => l
@@ -74,7 +74,7 @@
 
 val prop_of_vc =
   let
-    fun mk_conj t u = @{term "op &"} $ t $ u
+    fun mk_conj t u = @{term HOL.conj} $ t $ u
 
     fun term_of (Assume (t, v)) = @{term HOL.implies} $ t $ term_of v
       | term_of (Assert ((n, t), v)) =
diff -r 2d638e963357 -r 848be46708dc src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Aug 27 10:56:46 2010 +0200
@@ -1952,9 +1952,9 @@
         | NONE => error "num_of_term: unsupported dvd")
   | fm_of_term ps vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
       @{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2)
-  | fm_of_term ps vs (@{term "op &"} $ t1 $ t2) =
+  | fm_of_term ps vs (@{term HOL.conj} $ t1 $ t2) =
       @{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
-  | fm_of_term ps vs (@{term "op |"} $ t1 $ t2) =
+  | fm_of_term ps vs (@{term HOL.disj} $ t1 $ t2) =
       @{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
   | fm_of_term ps vs (@{term HOL.implies} $ t1 $ t2) =
       @{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
@@ -2016,7 +2016,7 @@
 
 fun term_bools acc t =
   let
-    val is_op = member (op =) [@{term "op &"}, @{term "op |"}, @{term HOL.implies}, @{term "op = :: bool => _"},
+    val is_op = member (op =) [@{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "op = :: bool => _"},
       @{term "op = :: int => _"}, @{term "op < :: int => _"},
       @{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"},
       @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]
diff -r 2d638e963357 -r 848be46708dc src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 27 10:56:46 2010 +0200
@@ -1996,8 +1996,8 @@
       @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) 
   | fm_of_term vs (@{term "op \<longleftrightarrow> :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
       @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
+  | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
+  | fm_of_term vs (@{term HOL.disj} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
   | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
   | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
   | fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
diff -r 2d638e963357 -r 848be46708dc src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Fri Aug 27 10:56:46 2010 +0200
@@ -5837,9 +5837,9 @@
       @{code Dvd} (HOLogic.dest_numeral t1, num_of_term vs t2)
   | fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
       @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (@{term "op &"} $ t1 $ t2) =
+  | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) =
       @{code And} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (@{term "op |"} $ t1 $ t2) =
+  | fm_of_term vs (@{term HOL.disj} $ t1 $ t2) =
       @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
   | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) =
       @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
diff -r 2d638e963357 -r 848be46708dc src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Aug 27 10:56:46 2010 +0200
@@ -2954,8 +2954,8 @@
 fun powt rT = Const(@{const_name "power"}, [rT,@{typ "nat"}] ---> rT);
 val brT = [bT, bT] ---> bT;
 val nott = @{term "Not"};
-val conjt = @{term "op &"};
-val disjt = @{term "op |"};
+val conjt = @{term HOL.conj};
+val disjt = @{term HOL.disj};
 val impt = @{term HOL.implies};
 val ifft = @{term "op = :: bool => _"}
 fun llt rT = Const(@{const_name Orderings.less},rrT rT);
@@ -3018,8 +3018,8 @@
     Const(@{const_name True},_) => @{code T}
   | Const(@{const_name False},_) => @{code F}
   | Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
-  | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
-  | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
+  | Const(@{const_name HOL.conj},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
+  | Const(@{const_name HOL.disj},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
   | Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
   | Const(@{const_name "op ="},ty)$p$q => 
        if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
diff -r 2d638e963357 -r 848be46708dc src/HOL/Decision_Procs/ferrante_rackoff.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -33,12 +33,12 @@
              {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
 let
  fun uset (vars as (x::vs)) p = case term_of p of
-   Const(@{const_name "op &"}, _)$ _ $ _ =>
+   Const(@{const_name HOL.conj}, _)$ _ $ _ =>
      let
        val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
        val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
      in (lS@rS, Drule.binop_cong_rule b lth rth) end
- |  Const(@{const_name "op |"}, _)$ _ $ _ =>
+ |  Const(@{const_name HOL.disj}, _)$ _ $ _ =>
      let
        val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
        val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
@@ -122,12 +122,12 @@
 
    fun decomp_mpinf fm =
      case term_of fm of
-       Const(@{const_name "op &"},_)$_$_ =>
+       Const(@{const_name HOL.conj},_)$_$_ =>
         let val (p,q) = Thm.dest_binop fm
         in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
                          (Thm.cabs x p) (Thm.cabs x q))
         end
-     | Const(@{const_name "op |"},_)$_$_ =>
+     | Const(@{const_name HOL.disj},_)$_$_ =>
         let val (p,q) = Thm.dest_binop fm
         in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
                          (Thm.cabs x p) (Thm.cabs x q))
@@ -181,8 +181,8 @@
    | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
    | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
-   | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
-   | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
    | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
    | Const ("==>", _) $ _ $ _ => find_args bounds tm
    | Const ("==", _) $ _ $ _ => find_args bounds tm
diff -r 2d638e963357 -r 848be46708dc src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -69,28 +69,28 @@
 val all_conjuncts = 
  let fun h acc ct = 
   case term_of ct of
-   @{term "op &"}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
+   @{term HOL.conj}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
   | _ => ct::acc
 in h [] end;
 
 fun conjuncts ct =
  case term_of ct of
-  @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
+  @{term HOL.conj}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
 | _ => [ct];
 
 fun fold1 f = foldr1 (uncurry f);
 
-val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ;
+val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm HOL.conj} c) c') ;
 
 fun mk_conj_tab th = 
  let fun h acc th = 
    case prop_of th of
-   @{term "Trueprop"}$(@{term "op &"}$p$q) => 
+   @{term "Trueprop"}$(@{term HOL.conj}$p$q) => 
      h (h acc (th RS conjunct2)) (th RS conjunct1)
   | @{term "Trueprop"}$p => (p,th)::acc
 in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
 
-fun is_conj (@{term "op &"}$_$_) = true
+fun is_conj (@{term HOL.conj}$_$_) = true
   | is_conj _ = false;
 
 fun prove_conj tab cjs = 
@@ -183,8 +183,8 @@
    | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
-   | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
-   | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
    | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
    | Const ("==>", _) $ _ $ _ => find_args bounds tm
    | Const ("==", _) $ _ $ _ => find_args bounds tm
diff -r 2d638e963357 -r 848be46708dc src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/HOL.thy	Fri Aug 27 10:56:46 2010 +0200
@@ -56,14 +56,14 @@
   True          :: bool
   False         :: bool
   Not           :: "bool => bool"                   ("~ _" [40] 40)
+
+  conj          :: "[bool, bool] => bool"           (infixr "&" 35)
+  disj          :: "[bool, bool] => bool"           (infixr "|" 30)
   implies       :: "[bool, bool] => bool"           (infixr "-->" 25)
 
 setup Sign.root_path
 
 consts
-  "op &"        :: "[bool, bool] => bool"           (infixr "&" 35)
-  "op |"        :: "[bool, bool] => bool"           (infixr "|" 30)
-
   "op ="        :: "['a, 'a] => bool"               (infixl "=" 50)
 
 setup Sign.local_path
@@ -89,15 +89,15 @@
 
 notation (xsymbols)
   Not  ("\<not> _" [40] 40) and
-  "op &"  (infixr "\<and>" 35) and
-  "op |"  (infixr "\<or>" 30) and
+  HOL.conj  (infixr "\<and>" 35) and
+  HOL.disj  (infixr "\<or>" 30) and
   HOL.implies  (infixr "\<longrightarrow>" 25) and
   not_equal  (infix "\<noteq>" 50)
 
 notation (HTML output)
   Not  ("\<not> _" [40] 40) and
-  "op &"  (infixr "\<and>" 35) and
-  "op |"  (infixr "\<or>" 30) and
+  HOL.conj  (infixr "\<and>" 35) and
+  HOL.disj  (infixr "\<or>" 30) and
   not_equal  (infix "\<noteq>" 50)
 
 abbreviation (iff)
@@ -1578,7 +1578,7 @@
   val atomize_conjL = @{thm atomize_conjL}
   val atomize_disjL = @{thm atomize_disjL}
   val operator_names =
-    [@{const_name "op |"}, @{const_name "op &"}, @{const_name Ex}]
+    [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}]
 );
 *}
 
@@ -1737,8 +1737,8 @@
   "True"    ("true")
   "False"   ("false")
   "Not"     ("Bool.not")
-  "op |"    ("(_ orelse/ _)")
-  "op &"    ("(_ andalso/ _)")
+  HOL.disj    ("(_ orelse/ _)")
+  HOL.conj    ("(_ andalso/ _)")
   "If"      ("(if _/ then _/ else _)")
 
 setup {*
@@ -1914,7 +1914,7 @@
   (Haskell "Bool")
   (Scala "Boolean")
 
-code_const True and False and Not and "op &" and "op |" and If
+code_const True and False and Not and HOL.conj and HOL.disj and If
   (SML "true" and "false" and "not"
     and infixl 1 "andalso" and infixl 0 "orelse"
     and "!(if (_)/ then (_)/ else (_))")
diff -r 2d638e963357 -r 848be46708dc src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Aug 27 10:56:46 2010 +0200
@@ -17,8 +17,8 @@
   T               > True
   F               > False
   "!"             > All
-  "/\\"           > "op &"
-  "\\/"           > "op |"
+  "/\\"           > HOL.conj
+  "\\/"           > HOL.disj
   "?"             > Ex
   "?!"            > Ex1
   "~"             > Not
diff -r 2d638e963357 -r 848be46708dc src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Aug 27 10:56:46 2010 +0200
@@ -55,8 +55,8 @@
   ONTO    > Fun.surj
   "=" > "op ="
   "==>" > HOL.implies
-  "/\\" > "op &"
-  "\\/" > "op |"
+  "/\\" > HOL.conj
+  "\\/" > HOL.disj
   "!" > All
   "?" > Ex
   "?!" > Ex1
diff -r 2d638e963357 -r 848be46708dc src/HOL/Import/HOL/bool.imp
--- a/src/HOL/Import/HOL/bool.imp	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Import/HOL/bool.imp	Fri Aug 27 10:56:46 2010 +0200
@@ -14,7 +14,7 @@
 const_maps
   "~" > "HOL.Not"
   "bool_case" > "Datatype.bool.bool_case"
-  "\\/" > "op |"
+  "\\/" > HOL.disj
   "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
   "T" > "HOL.True"
   "RES_SELECT" > "HOL4Base.bool.RES_SELECT"
@@ -30,7 +30,7 @@
   "ARB" > "HOL4Base.bool.ARB"
   "?!" > "HOL.Ex1"
   "?" > "HOL.Ex"
-  "/\\" > "op &"
+  "/\\" > HOL.conj
   "!" > "HOL.All"
 
 thm_maps
diff -r 2d638e963357 -r 848be46708dc src/HOL/Import/HOLLight/hollight.imp
--- a/src/HOL/Import/HOLLight/hollight.imp	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp	Fri Aug 27 10:56:46 2010 +0200
@@ -115,7 +115,7 @@
   "_10303" > "HOLLight.hollight._10303"
   "_10302" > "HOLLight.hollight._10302"
   "_0" > "0" :: "nat"
-  "\\/" > "op |"
+  "\\/" > HOL.disj
   "ZRECSPACE" > "HOLLight.hollight.ZRECSPACE"
   "ZIP" > "HOLLight.hollight.ZIP"
   "ZCONSTR" > "HOLLight.hollight.ZCONSTR"
@@ -237,7 +237,7 @@
   "=" > "op ="
   "<=" > "HOLLight.hollight.<="
   "<" > "HOLLight.hollight.<"
-  "/\\" > "op &"
+  "/\\" > HOL.conj
   "-" > "Groups.minus" :: "nat => nat => nat"
   "," > "Product_Type.Pair"
   "+" > "Groups.plus" :: "nat => nat => nat"
diff -r 2d638e963357 -r 848be46708dc src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -1205,7 +1205,7 @@
 fun non_trivial_term_consts t = fold_aterms
   (fn Const (c, _) =>
       if c = @{const_name Trueprop} orelse c = @{const_name All}
-        orelse c = @{const_name HOL.implies} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
+        orelse c = @{const_name HOL.implies} orelse c = @{const_name HOL.conj} orelse c = @{const_name "op ="}
       then I else insert (op =) c
     | _ => I) t [];
 
@@ -1217,7 +1217,7 @@
                | @{const_name HOL.implies} => insert (op =) "==>" cs
                | @{const_name All} => cs
                | "all" => cs
-               | @{const_name "op &"} => cs
+               | @{const_name HOL.conj} => cs
                | @{const_name Trueprop} => cs
                | _ => insert (op =) c cs)
           | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
@@ -1521,7 +1521,7 @@
         val th1 = norm_hyps th1
         val th2 = norm_hyps th2
         val (l,r) = case concl_of th of
-                        _ $ (Const(@{const_name "op |"},_) $ l $ r) => (l,r)
+                        _ $ (Const(@{const_name HOL.disj},_) $ l $ r) => (l,r)
                       | _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction"
         val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1
         val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2
diff -r 2d638e963357 -r 848be46708dc src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -1356,7 +1356,7 @@
 
 val known_sos_constants =
   [@{term "op ==>"}, @{term "Trueprop"},
-   @{term HOL.implies}, @{term "op &"}, @{term "op |"},
+   @{term HOL.implies}, @{term HOL.conj}, @{term HOL.disj},
    @{term "Not"}, @{term "op = :: bool => _"},
    @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"},
    @{term "op = :: real => _"}, @{term "op < :: real => _"},
diff -r 2d638e963357 -r 848be46708dc src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -439,8 +439,8 @@
   val is_req = is_binop @{cterm "op =:: real => _"}
   val is_ge = is_binop @{cterm "op <=:: real => _"}
   val is_gt = is_binop @{cterm "op <:: real => _"}
-  val is_conj = is_binop @{cterm "op &"}
-  val is_disj = is_binop @{cterm "op |"}
+  val is_conj = is_binop @{cterm HOL.conj}
+  val is_disj = is_binop @{cterm HOL.disj}
   fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
   fun disj_cases th th1 th2 = 
    let val (p,q) = Thm.dest_binop (concl th)
@@ -484,7 +484,7 @@
     val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
     val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
     val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
-    val th' = Drule.binop_cong_rule @{cterm "op |"} 
+    val th' = Drule.binop_cong_rule @{cterm HOL.disj} 
      (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
      (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
     in Thm.transitive th th' 
@@ -542,12 +542,12 @@
   let 
    val nnf_norm_conv' = 
      nnf_conv then_conv 
-     literals_conv [@{term "op &"}, @{term "op |"}] [] 
+     literals_conv [@{term HOL.conj}, @{term HOL.disj}] [] 
      (Conv.cache_conv 
        (first_conv [real_lt_conv, real_le_conv, 
                     real_eq_conv, real_not_lt_conv, 
                     real_not_le_conv, real_not_eq_conv, all_conv]))
-  fun absremover ct = (literals_conv [@{term "op &"}, @{term "op |"}] [] 
+  fun absremover ct = (literals_conv [@{term HOL.conj}, @{term HOL.disj}] [] 
                   (try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv 
         try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct
   val nct = Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"} ct)
diff -r 2d638e963357 -r 848be46708dc src/HOL/Mutabelle/Mutabelle.thy
--- a/src/HOL/Mutabelle/Mutabelle.thy	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Mutabelle/Mutabelle.thy	Fri Aug 27 10:56:46 2010 +0200
@@ -4,7 +4,7 @@
 begin
 
 ML {*
-val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}];
+val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}];
 
 val forbidden =
  [(@{const_name Power.power}, "'a"),
diff -r 2d638e963357 -r 848be46708dc src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -187,7 +187,7 @@
 val nitpick_mtd = ("nitpick", invoke_nitpick)
 *)
 
-val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}]
+val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}]
 
 val forbidden =
  [(* (@{const_name "power"}, "'a"), *)
diff -r 2d638e963357 -r 848be46708dc src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -1200,7 +1200,7 @@
           (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
     val tnames = Datatype_Prop.make_tnames recTs;
     val zs = Name.variant_list tnames (replicate (length descr'') "z");
-    val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+    val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
       (map (fn ((((i, _), T), tname), z) =>
         make_pred fsT i T $ Free (z, fsT) $ Free (tname, T))
         (descr'' ~~ recTs ~~ tnames ~~ zs)));
@@ -1215,7 +1215,7 @@
         map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
           HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
             (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
-    val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+    val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
       (map (fn ((((i, _), T), tname), z) =>
         make_pred fsT' i T $ Free (z, fsT') $ Free (tname, T))
         (descr'' ~~ recTs ~~ tnames ~~ zs)));
@@ -1225,7 +1225,7 @@
       (Datatype_Prop.indexify_names (replicate (length dt_atomTs) "pi") ~~
        map mk_permT dt_atomTs) @ [("z", fsT')];
     val aux_ind_Ts = rev (map snd aux_ind_vars);
-    val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+    val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
       (map (fn (((i, _), T), tname) =>
         HOLogic.list_all (aux_ind_vars, make_pred fsT' i T $ Bound 0 $
           fold_rev (mk_perm aux_ind_Ts) (map Bound (length dt_atomTs downto 1))
diff -r 2d638e963357 -r 848be46708dc src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -71,7 +71,7 @@
   | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
   | add_binders thy i _ bs = bs;
 
-fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
+fun split_conj f names (Const (@{const_name HOL.conj}, _) $ p $ q) _ = (case head_of p of
       Const (name, _) =>
         if member (op =) names name then SOME (f p q) else NONE
     | _ => NONE)
@@ -89,7 +89,7 @@
 (* where "id" protects the subformula from simplification            *)
 (*********************************************************************)
 
-fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
+fun inst_conj_all names ps pis (Const (@{const_name HOL.conj}, _) $ p $ q) _ =
       (case head_of p of
          Const (name, _) =>
            if member (op =) names name then SOME (HOLogic.mk_conj (p,
diff -r 2d638e963357 -r 848be46708dc src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -76,7 +76,7 @@
   | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
   | add_binders thy i _ bs = bs;
 
-fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
+fun split_conj f names (Const (@{const_name HOL.conj}, _) $ p $ q) _ = (case head_of p of
       Const (name, _) =>
         if member (op =) names name then SOME (f p q) else NONE
     | _ => NONE)
@@ -94,7 +94,7 @@
 (* where "id" protects the subformula from simplification            *)
 (*********************************************************************)
 
-fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
+fun inst_conj_all names ps pis (Const (@{const_name HOL.conj}, _) $ p $ q) _ =
       (case head_of p of
          Const (name, _) =>
            if member (op =) names name then SOME (HOLogic.mk_conj (p,
diff -r 2d638e963357 -r 848be46708dc src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Orderings.thy	Fri Aug 27 10:56:46 2010 +0200
@@ -641,7 +641,7 @@
   val All_binder = Syntax.binder_name @{const_syntax All};
   val Ex_binder = Syntax.binder_name @{const_syntax Ex};
   val impl = @{const_syntax HOL.implies};
-  val conj = @{const_syntax "op &"};
+  val conj = @{const_syntax HOL.conj};
   val less = @{const_syntax less};
   val less_eq = @{const_syntax less_eq};
 
diff -r 2d638e963357 -r 848be46708dc src/HOL/Prolog/prolog.ML
--- a/src/HOL/Prolog/prolog.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Prolog/prolog.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -11,12 +11,12 @@
 
 fun isD t = case t of
     Const(@{const_name Trueprop},_)$t     => isD t
-  | Const(@{const_name "op &"}  ,_)$l$r     => isD l andalso isD r
+  | Const(@{const_name HOL.conj}  ,_)$l$r     => isD l andalso isD r
   | Const(@{const_name HOL.implies},_)$l$r     => isG l andalso isD r
   | Const(   "==>",_)$l$r     => isG l andalso isD r
   | Const(@{const_name All},_)$Abs(s,_,t) => isD t
   | Const("all",_)$Abs(s,_,t) => isD t
-  | Const(@{const_name "op |"},_)$_$_       => false
+  | Const(@{const_name HOL.disj},_)$_$_       => false
   | Const(@{const_name Ex} ,_)$_          => false
   | Const(@{const_name Not},_)$_          => false
   | Const(@{const_name True},_)           => false
@@ -30,8 +30,8 @@
 and
     isG t = case t of
     Const(@{const_name Trueprop},_)$t     => isG t
-  | Const(@{const_name "op &"}  ,_)$l$r     => isG l andalso isG r
-  | Const(@{const_name "op |"}  ,_)$l$r     => isG l andalso isG r
+  | Const(@{const_name HOL.conj}  ,_)$l$r     => isG l andalso isG r
+  | Const(@{const_name HOL.disj}  ,_)$l$r     => isG l andalso isG r
   | Const(@{const_name HOL.implies},_)$l$r     => isD l andalso isG r
   | Const(   "==>",_)$l$r     => isD l andalso isG r
   | Const(@{const_name All},_)$Abs(_,_,t) => isG t
@@ -53,7 +53,7 @@
     fun at  thm = case concl_of thm of
       _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
         (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
-    | _$(Const(@{const_name "op &"},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
+    | _$(Const(@{const_name HOL.conj},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
     | _$(Const(@{const_name HOL.implies},_)$_$_)     => at(thm RS mp)
     | _                             => [thm]
 in map zero_var_indexes (at thm) end;
diff -r 2d638e963357 -r 848be46708dc src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Set.thy	Fri Aug 27 10:56:46 2010 +0200
@@ -220,7 +220,7 @@
   val All_binder = Syntax.binder_name @{const_syntax All};
   val Ex_binder = Syntax.binder_name @{const_syntax Ex};
   val impl = @{const_syntax HOL.implies};
-  val conj = @{const_syntax "op &"};
+  val conj = @{const_syntax HOL.conj};
   val sbset = @{const_syntax subset};
   val sbset_eq = @{const_syntax subset_eq};
 
@@ -269,7 +269,7 @@
     fun setcompr_tr [e, idts, b] =
       let
         val eq = Syntax.const @{const_syntax "op ="} $ Bound (nvars idts) $ e;
-        val P = Syntax.const @{const_syntax "op &"} $ eq $ b;
+        val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
         val exP = ex_tr [idts, P];
       in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
 
@@ -288,7 +288,7 @@
   fun setcompr_tr' [Abs (abs as (_, _, P))] =
     let
       fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
-        | check (Const (@{const_syntax "op &"}, _) $
+        | check (Const (@{const_syntax HOL.conj}, _) $
               (Const (@{const_syntax "op ="}, _) $ Bound m $ e) $ P, n) =
             n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
             subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
@@ -305,7 +305,7 @@
           val M = Syntax.const @{syntax_const "_Coll"} $ x $ t;
         in
           case t of
-            Const (@{const_syntax "op &"}, _) $
+            Const (@{const_syntax HOL.conj}, _) $
               (Const (@{const_syntax Set.member}, _) $
                 (Const (@{syntax_const "_bound"}, _) $ Free (yN, _)) $ A) $ P =>
             if xN = yN then Syntax.const @{syntax_const "_Collect"} $ x $ A $ P else M
diff -r 2d638e963357 -r 848be46708dc src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -53,7 +53,7 @@
 val lazy_conj_simproc =
   Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"]
     (fn thy => fn ss => fn t =>
-      (case t of (Const (@{const_name "op &"},_)$P$Q) => 
+      (case t of (Const (@{const_name HOL.conj},_)$P$Q) => 
          let
             val P_P' = Simplifier.rewrite ss (cterm_of thy P);
             val P' = P_P' |> prop_of |> Logic.dest_equals |> #2 
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Datatype/datatype_aux.ML
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -120,8 +120,8 @@
 fun split_conj_thm th =
   ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th];
 
-val mk_conj = foldr1 (HOLogic.mk_binop @{const_name "op &"});
-val mk_disj = foldr1 (HOLogic.mk_binop @{const_name "op |"});
+val mk_conj = foldr1 (HOLogic.mk_binop @{const_name HOL.conj});
+val mk_disj = foldr1 (HOLogic.mk_binop @{const_name HOL.disj});
 
 fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
 
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Datatype/datatype_prop.ML
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -70,7 +70,7 @@
           val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
         in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
           (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
-           foldr1 (HOLogic.mk_binop @{const_name "op &"})
+           foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
              (map HOLogic.mk_eq (frees ~~ frees')))))
         end;
   in
@@ -149,7 +149,7 @@
     val prems = maps (fn ((i, (_, _, constrs)), T) =>
       map (make_ind_prem i T) constrs) (descr' ~~ recTs);
     val tnames = make_tnames recTs;
-    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
+    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
       (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
         (descr' ~~ recTs ~~ tnames)))
 
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -99,7 +99,7 @@
         if member (op =) is i then SOME
           (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
         else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
-    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
+    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
       (map (fn ((((i, _), T), U), tname) =>
         make_pred i U T (mk_proj i is r) (Free (tname, T)))
           (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -148,7 +148,7 @@
     val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
     fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
       let
-        val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
+        val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
           = Term.strip_qnt_body @{const_name Ex} c
       in cons r o cons l end
   in
@@ -185,7 +185,7 @@
     val vs = Term.strip_qnt_vars @{const_name Ex} c
 
     (* FIXME: throw error "dest_call" for malformed terms *)
-    val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
+    val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
       = Term.strip_qnt_body @{const_name Ex} c
     val (p, l') = dest_inj sk l
     val (q, r') = dest_inj sk r
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Nitpick/minipick.ML
--- a/src/HOL/Tools/Nitpick/minipick.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -130,8 +130,8 @@
                       [Type (@{type_name fun}, [_, @{typ bool}]), _]))
          $ t1 $ t2 =>
          Subset (to_R_rep Ts t1, to_R_rep Ts t2)
-       | @{const "op &"} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
-       | @{const "op |"} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
+       | @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
+       | @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
        | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
        | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
        | Free _ => raise SAME ()
@@ -173,10 +173,10 @@
          to_R_rep Ts (eta_expand Ts t 1)
        | Const (@{const_name ord_class.less_eq}, _) =>
          to_R_rep Ts (eta_expand Ts t 2)
-       | @{const "op &"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
-       | @{const "op &"} => to_R_rep Ts (eta_expand Ts t 2)
-       | @{const "op |"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
-       | @{const "op |"} => to_R_rep Ts (eta_expand Ts t 2)
+       | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+       | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
+       | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+       | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
        | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
        | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
        | Const (@{const_name bot_class.bot},
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -386,13 +386,13 @@
     if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
   | strip_connective _ t = [t]
 fun strip_any_connective (t as (t0 $ _ $ _)) =
-    if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
+    if t0 = @{const HOL.conj} orelse t0 = @{const HOL.disj} then
       (strip_connective t0 t, t0)
     else
       ([t], @{const Not})
   | strip_any_connective t = ([t], @{const Not})
-val conjuncts_of = strip_connective @{const "op &"}
-val disjuncts_of = strip_connective @{const "op |"}
+val conjuncts_of = strip_connective @{const HOL.conj}
+val disjuncts_of = strip_connective @{const HOL.disj}
 
 (* When you add constants to these lists, make sure to handle them in
    "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
@@ -409,8 +409,8 @@
    (@{const_name All}, 1),
    (@{const_name Ex}, 1),
    (@{const_name "op ="}, 1),
-   (@{const_name "op &"}, 2),
-   (@{const_name "op |"}, 2),
+   (@{const_name HOL.conj}, 2),
+   (@{const_name HOL.disj}, 2),
    (@{const_name HOL.implies}, 2),
    (@{const_name If}, 3),
    (@{const_name Let}, 2),
@@ -2148,8 +2148,8 @@
           fun repair_rec j (Const (@{const_name Ex}, T1) $ Abs (s2, T2, t2')) =
               Const (@{const_name Ex}, T1)
               $ Abs (s2, T2, repair_rec (j + 1) t2')
-            | repair_rec j (@{const "op &"} $ t1 $ t2) =
-              @{const "op &"} $ repair_rec j t1 $ repair_rec j t2
+            | repair_rec j (@{const HOL.conj} $ t1 $ t2) =
+              @{const HOL.conj} $ repair_rec j t1 $ repair_rec j t2
             | repair_rec j t =
               let val (head, args) = strip_comb t in
                 if head = Bound j then
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -777,7 +777,7 @@
            $ Abs (s', T', (t10 as @{const HOL.implies}) $ (t11 $ Bound 0) $ t12) =>
            do_bounded_quantifier t0 s' T' t10 t11 t12 accum
          | (t0 as Const (@{const_name Ex}, _))
-           $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
+           $ Abs (s', T', (t10 as @{const HOL.conj}) $ (t11 $ Bound 0) $ t12) =>
            do_bounded_quantifier t0 s' T' t10 t11 t12 accum
          | Const (@{const_name Let}, _) $ t1 $ t2 =>
            do_term (betapply (t2, t1)) accum
@@ -883,8 +883,8 @@
            | (t0 as Const (s0, _)) $ t1 $ t2 =>
              if s0 = @{const_name "==>"} orelse
                 s0 = @{const_name Pure.conjunction} orelse
-                s0 = @{const_name "op &"} orelse
-                s0 = @{const_name "op |"} orelse
+                s0 = @{const_name HOL.conj} orelse
+                s0 = @{const_name HOL.disj} orelse
                 s0 = @{const_name HOL.implies} then
                let
                  val impl = (s0 = @{const_name "==>"} orelse
@@ -975,7 +975,7 @@
             do_all t0 s0 T1 t1 accum
           | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
             consider_general_equals mdata true x t1 t2 accum
-          | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
+          | (t0 as @{const HOL.conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
           | (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
           | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
                              \do_formula", [t])
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -518,9 +518,9 @@
         | (Const (@{const_name "op ="}, T), [t1]) =>
           Op1 (SingletonSet, range_type T, Any, sub t1)
         | (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2
-        | (Const (@{const_name "op &"}, _), [t1, t2]) =>
+        | (Const (@{const_name HOL.conj}, _), [t1, t2]) =>
           Op2 (And, bool_T, Any, sub' t1, sub' t2)
-        | (Const (@{const_name "op |"}, _), [t1, t2]) =>
+        | (Const (@{const_name HOL.disj}, _), [t1, t2]) =>
           Op2 (Or, bool_T, Any, sub t1, sub t2)
         | (Const (@{const_name HOL.implies}, _), [t1, t2]) =>
           Op2 (Or, bool_T, Any, Op1 (Not, bool_T, Any, sub t1), sub' t2)
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -211,11 +211,11 @@
         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
       | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
         do_equals new_Ts old_Ts s0 T0 t1 t2
-      | @{const "op &"} $ t1 $ t2 =>
-        @{const "op &"} $ do_term new_Ts old_Ts polar t1
+      | @{const HOL.conj} $ t1 $ t2 =>
+        @{const HOL.conj} $ do_term new_Ts old_Ts polar t1
         $ do_term new_Ts old_Ts polar t2
-      | @{const "op |"} $ t1 $ t2 =>
-        @{const "op |"} $ do_term new_Ts old_Ts polar t1
+      | @{const HOL.disj} $ t1 $ t2 =>
+        @{const HOL.disj} $ do_term new_Ts old_Ts polar t1
         $ do_term new_Ts old_Ts polar t2
       | @{const HOL.implies} $ t1 $ t2 =>
         @{const HOL.implies} $ do_term new_Ts old_Ts (flip_polarity polar) t1
@@ -449,7 +449,7 @@
 (** Destruction of universal and existential equalities **)
 
 fun curry_assms (@{const "==>"} $ (@{const Trueprop}
-                                   $ (@{const "op &"} $ t1 $ t2)) $ t3) =
+                                   $ (@{const HOL.conj} $ t1 $ t2)) $ t3) =
     curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
   | curry_assms (@{const "==>"} $ t1 $ t2) =
     @{const "==>"} $ curry_assms t1 $ curry_assms t2
@@ -604,9 +604,9 @@
           do_quantifier s0 T0 s1 T1 t1
         | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
           do_quantifier s0 T0 s1 T1 t1
-        | @{const "op &"} $ t1 $ t2 =>
+        | @{const HOL.conj} $ t1 $ t2 =>
           s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
-        | @{const "op |"} $ t1 $ t2 =>
+        | @{const HOL.disj} $ t1 $ t2 =>
           s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
         | @{const HOL.implies} $ t1 $ t2 =>
           @{const HOL.implies} $ aux ss Ts js skolemizable (flip_polarity polar) t1
@@ -620,8 +620,8 @@
             let
               val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
               val (pref, connective) =
-                if gfp then (lbfp_prefix, @{const "op |"})
-                else (ubfp_prefix, @{const "op &"})
+                if gfp then (lbfp_prefix, @{const HOL.disj})
+                else (ubfp_prefix, @{const HOL.conj})
               fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
                            |> aux ss Ts js skolemizable polar
               fun neg () = Const (pref ^ s, T)
@@ -1105,7 +1105,7 @@
   case t of
     (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
     (case t1 of
-       (t10 as @{const "op &"}) $ t11 $ t12 =>
+       (t10 as @{const HOL.conj}) $ t11 $ t12 =>
        t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
      | (t10 as @{const Not}) $ t11 =>
@@ -1118,7 +1118,7 @@
          t0 $ Abs (s, T1, distribute_quantifiers t1))
   | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
     (case distribute_quantifiers t1 of
-       (t10 as @{const "op |"}) $ t11 $ t12 =>
+       (t10 as @{const HOL.disj}) $ t11 $ t12 =>
        t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
      | (t10 as @{const HOL.implies}) $ t11 $ t12 =>
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -405,7 +405,7 @@
 (* general syntactic functions *)
 
 (*Like dest_conj, but flattens conjunctions however nested*)
-fun conjuncts_aux (Const (@{const_name "op &"}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
+fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
   | conjuncts_aux t conjs = t::conjs;
 
 fun conjuncts t = conjuncts_aux t [];
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -524,7 +524,7 @@
 
 fun dest_conjunct_prem th =
   case HOLogic.dest_Trueprop (prop_of th) of
-    (Const (@{const_name "op &"}, _) $ t $ t') =>
+    (Const (@{const_name HOL.conj}, _) $ t $ t') =>
       dest_conjunct_prem (th RS @{thm conjunct1})
         @ dest_conjunct_prem (th RS @{thm conjunct2})
     | _ => [th]
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -221,8 +221,8 @@
    @{const_name HOL.implies},
    @{const_name All},
    @{const_name Ex}, 
-   @{const_name "op &"},
-   @{const_name "op |"}]
+   @{const_name HOL.conj},
+   @{const_name HOL.disj}]
 
 fun special_cases (c, T) = member (op =) [
   @{const_name Product_Type.Unity},
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -89,8 +89,8 @@
 fun is_compound ((Const (@{const_name Not}, _)) $ t) =
     error "is_compound: Negation should not occur; preprocessing is defect"
   | is_compound ((Const (@{const_name Ex}, _)) $ _) = true
-  | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
-  | is_compound ((Const (@{const_name "op &"}, _)) $ _ $ _) =
+  | is_compound ((Const (@{const_name HOL.disj}, _)) $ _ $ _) = true
+  | is_compound ((Const (@{const_name HOL.conj}, _)) $ _ $ _) =
     error "is_compound: Conjunction should not occur; preprocessing is defect"
   | is_compound _ = false
 
@@ -250,7 +250,7 @@
 
 fun split_conjs thy t =
   let 
-    fun split_conjunctions (Const (@{const_name "op &"}, _) $ t1 $ t2) =
+    fun split_conjunctions (Const (@{const_name HOL.conj}, _) $ t1 $ t2) =
     (split_conjunctions t1) @ (split_conjunctions t2)
     | split_conjunctions t = [t]
   in
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -28,7 +28,7 @@
    @{term "op * :: int => _"}, @{term "op * :: nat => _"},
    @{term "op div :: int => _"}, @{term "op div :: nat => _"},
    @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
-   @{term "op &"}, @{term "op |"}, @{term HOL.implies}, 
+   @{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, 
    @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
    @{term "op < :: int => _"}, @{term "op < :: nat => _"},
    @{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
@@ -120,8 +120,8 @@
 
 fun whatis x ct =
 ( case (term_of ct) of
-  Const(@{const_name "op &"},_)$_$_ => And (Thm.dest_binop ct)
-| Const (@{const_name "op |"},_)$_$_ => Or (Thm.dest_binop ct)
+  Const(@{const_name HOL.conj},_)$_$_ => And (Thm.dest_binop ct)
+| Const (@{const_name HOL.disj},_)$_$_ => Or (Thm.dest_binop ct)
 | Const (@{const_name "op ="},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
 | Const (@{const_name Not},_) $ (Const (@{const_name "op ="},_)$y$_) =>
   if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
@@ -353,8 +353,8 @@
     then (ins (dest_number c) acc, dacc) else (acc,dacc)
   | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
     if x aconv y then (acc,ins (dest_number c) dacc) else (acc,dacc)
-  | Const(@{const_name "op &"},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
-  | Const(@{const_name "op |"},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
+  | Const(@{const_name HOL.conj},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
+  | Const(@{const_name HOL.disj},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
   | _ => (acc, dacc)
   val (cs,ds) = h ([],[]) p
@@ -382,8 +382,8 @@
     end
   fun unit_conv t =
    case (term_of t) of
-   Const(@{const_name "op &"},_)$_$_ => Conv.binop_conv unit_conv t
-  | Const(@{const_name "op |"},_)$_$_ => Conv.binop_conv unit_conv t
+   Const(@{const_name HOL.conj},_)$_$_ => Conv.binop_conv unit_conv t
+  | Const(@{const_name HOL.disj},_)$_$_ => Conv.binop_conv unit_conv t
   | Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
   | Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
     if x=y andalso member (op =)
@@ -569,7 +569,7 @@
 fun add_bools t =
   let
     val ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"}, @{term "op <= :: int => _"},
-      @{term "op &"}, @{term "op |"}, @{term HOL.implies}, @{term "op = :: bool => _"},
+      @{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "op = :: bool => _"},
       @{term "Not"}, @{term "All :: (int => _) => _"},
       @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}];
     val is_op = member (op =) ops;
@@ -612,9 +612,9 @@
 
 fun fm_of_term ps vs (Const (@{const_name True}, _)) = Proc.T
   | fm_of_term ps vs (Const (@{const_name False}, _)) = Proc.F
-  | fm_of_term ps vs (Const (@{const_name "op &"}, _) $ t1 $ t2) =
+  | fm_of_term ps vs (Const (@{const_name HOL.conj}, _) $ t1 $ t2) =
       Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2)
-  | fm_of_term ps vs (Const (@{const_name "op |"}, _) $ t1 $ t2) =
+  | fm_of_term ps vs (Const (@{const_name HOL.disj}, _) $ t1 $ t2) =
       Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2)
   | fm_of_term ps vs (Const (@{const_name HOL.implies}, _) $ t1 $ t2) =
       Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2)
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Qelim/qelim.ML
--- a/src/HOL/Tools/Qelim/qelim.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -25,7 +25,7 @@
    case (term_of p) of
     Const(s,T)$_$_ => 
        if domain_type T = HOLogic.boolT
-          andalso member (op =) [@{const_name "op &"}, @{const_name "op |"},
+          andalso member (op =) [@{const_name HOL.conj}, @{const_name HOL.disj},
             @{const_name HOL.implies}, @{const_name "op ="}] s
        then binop_conv (conv env) p 
        else atcv env p
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -485,7 +485,7 @@
        end
 
   | (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
-      (Const (@{const_name "op &"}, _) $ (Const (@{const_name Set.member}, _) $ _ $
+      (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $
         (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
      Const (@{const_name Ex1}, ty') $ t') =>
        let
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -159,8 +159,8 @@
 fun conn @{const_name True} = SOME "true"
   | conn @{const_name False} = SOME "false"
   | conn @{const_name Not} = SOME "not"
-  | conn @{const_name "op &"} = SOME "and"
-  | conn @{const_name "op |"} = SOME "or"
+  | conn @{const_name HOL.conj} = SOME "and"
+  | conn @{const_name HOL.disj} = SOME "or"
   | conn @{const_name HOL.implies} = SOME "implies"
   | conn @{const_name "op ="} = SOME "iff"
   | conn @{const_name If} = SOME "if_then_else"
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -216,8 +216,8 @@
     (Sym ("true", _), []) => SOME mk_true
   | (Sym ("false", _), []) => SOME mk_false
   | (Sym ("not", _), [ct]) => SOME (mk_not ct)
-  | (Sym ("and", _), _) => SOME (mk_nary @{cterm "op &"} mk_true cts)
-  | (Sym ("or", _), _) => SOME (mk_nary @{cterm "op |"} mk_false cts)
+  | (Sym ("and", _), _) => SOME (mk_nary @{cterm HOL.conj} mk_true cts)
+  | (Sym ("or", _), _) => SOME (mk_nary @{cterm HOL.disj} mk_false cts)
   | (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu)
   | (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu)
   | (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu)
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/SMT/z3_proof_literals.ML
--- a/src/HOL/Tools/SMT/z3_proof_literals.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_literals.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -62,14 +62,14 @@
 val is_neg = (fn @{term Not} $ _ => true | _ => false)
 fun is_neg' f = (fn @{term Not} $ t => f t | _ => false)
 val is_dneg = is_neg' is_neg
-val is_conj = (fn @{term "op &"} $ _ $ _ => true | _ => false)
-val is_disj = (fn @{term "op |"} $ _ $ _ => true | _ => false)
+val is_conj = (fn @{term HOL.conj} $ _ $ _ => true | _ => false)
+val is_disj = (fn @{term HOL.disj} $ _ $ _ => true | _ => false)
 
 fun dest_disj_term' f = (fn
-    @{term Not} $ (@{term "op |"} $ t $ u) => SOME (f t, f u)
+    @{term Not} $ (@{term HOL.disj} $ t $ u) => SOME (f t, f u)
   | _ => NONE)
 
-val dest_conj_term = (fn @{term "op &"} $ t $ u => SOME (t, u) | _ => NONE)
+val dest_conj_term = (fn @{term HOL.conj} $ t $ u => SOME (t, u) | _ => NONE)
 val dest_disj_term =
   dest_disj_term' (fn @{term Not} $ t => t | t => @{term Not} $ t)
 
@@ -202,11 +202,11 @@
     | comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2
     | comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2
 
-  fun dest_conj (@{term "op &"} $ t $ u) = ((false, t), (false, u))
+  fun dest_conj (@{term HOL.conj} $ t $ u) = ((false, t), (false, u))
     | dest_conj t = raise TERM ("dest_conj", [t])
 
   val neg = (fn @{term Not} $ t => (true, t) | t => (false, @{term Not} $ t))
-  fun dest_disj (@{term Not} $ (@{term "op |"} $ t $ u)) = (neg t, neg u)
+  fun dest_disj (@{term Not} $ (@{term HOL.disj} $ t $ u)) = (neg t, neg u)
     | dest_disj t = raise TERM ("dest_disj", [t])
 
   val dnegE = T.precompose (single o d2 o d1) @{thm notnotD}
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -298,13 +298,13 @@
     let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
     in
       (case Thm.term_of ct1 of
-        @{term Not} $ (@{term "op &"} $ _ $ _) =>
+        @{term Not} $ (@{term HOL.conj} $ _ $ _) =>
           prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
-      | @{term "op &"} $ _ $ _ =>
+      | @{term HOL.conj} $ _ $ _ =>
           prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, true)
-      | @{term Not} $ (@{term "op |"} $ _ $ _) =>
+      | @{term Not} $ (@{term HOL.disj} $ _ $ _) =>
           prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, false)
-      | @{term "op |"} $ _ $ _ =>
+      | @{term HOL.disj} $ _ $ _ =>
           prove disjI2 (Thm.capply @{cterm Not} ct1, false) (ct2, true)
       | Const (@{const_name distinct}, _) $ _ =>
           let
@@ -477,8 +477,8 @@
 
   fun mono f (cp as (cl, _)) =
     (case Term.head_of (Thm.term_of cl) of
-      @{term "op &"} => prove_nary L.is_conj (prove_eq_exn f)
-    | @{term "op |"} => prove_nary L.is_disj (prove_eq_exn f)
+      @{term HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
+    | @{term HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
     | Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f)
     | _ => prove (prove_eq_safe f)) cp
 in
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -196,8 +196,8 @@
       | @{term True} => pair ct
       | @{term False} => pair ct
       | @{term Not} $ _ => abstr1 cvs ct
-      | @{term "op &"} $ _ $ _ => abstr2 cvs ct
-      | @{term "op |"} $ _ $ _ => abstr2 cvs ct
+      | @{term HOL.conj} $ _ $ _ => abstr2 cvs ct
+      | @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
       | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
       | Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
       | Const (@{const_name distinct}, _) $ _ =>
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -68,8 +68,8 @@
         (*Universal quant: insert a free variable into body and continue*)
         let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
         in dec_sko (subst_bound (Free(fname,T), p)) rhss end
-      | dec_sko (@{const "op &"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
-      | dec_sko (@{const "op |"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+      | dec_sko (@{const HOL.conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+      | dec_sko (@{const HOL.disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
       | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
       | dec_sko _ rhss = rhss
   in  dec_sko (prop_of th) []  end;
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Sledgehammer/metis_clauses.ML
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -95,8 +95,8 @@
   Symtab.make [(@{type_name Product_Type.prod}, "prod"),
                (@{type_name Sum_Type.sum}, "sum"),
                (@{const_name "op ="}, "equal"),
-               (@{const_name "op &"}, "and"),
-               (@{const_name "op |"}, "or"),
+               (@{const_name HOL.conj}, "and"),
+               (@{const_name HOL.disj}, "or"),
                (@{const_name HOL.implies}, "implies"),
                (@{const_name Set.member}, "member"),
                (@{const_name fequal}, "fequal"),
@@ -430,7 +430,7 @@
 
 fun literals_of_term1 args thy (@{const Trueprop} $ P) =
     literals_of_term1 args thy P
-  | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
+  | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
     literals_of_term1 (literals_of_term1 args thy P) thy Q
   | literals_of_term1 (lits, ts) thy P =
     let val ((pred, ts'), pol) = predicate_of thy (P, true) in
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -159,8 +159,8 @@
         do_quantifier (pos = SOME false) body_t
       | Const (@{const_name Ex}, _) $ Abs (_, _, body_t) =>
         do_quantifier (pos = SOME true) body_t
-      | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
-      | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+      | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+      | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
       | @{const HOL.implies} $ t1 $ t2 =>
         do_formula (flip pos) t1 #> do_formula pos t2
       | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
@@ -545,8 +545,8 @@
         do_formula (not pos) t1 andalso
         (t2 = @{const False} orelse do_formula pos t2)
       | (_, @{const Not} $ t1) => do_formula (not pos) t1
-      | (true, @{const "op |"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
-      | (false, @{const "op &"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+      | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+      | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
       | (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2
       | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
       | _ => false
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -70,11 +70,11 @@
   | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
     Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
   | negate_term (@{const HOL.implies} $ t1 $ t2) =
-    @{const "op &"} $ t1 $ negate_term t2
-  | negate_term (@{const "op &"} $ t1 $ t2) =
-    @{const "op |"} $ negate_term t1 $ negate_term t2
-  | negate_term (@{const "op |"} $ t1 $ t2) =
-    @{const "op &"} $ negate_term t1 $ negate_term t2
+    @{const HOL.conj} $ t1 $ negate_term t2
+  | negate_term (@{const HOL.conj} $ t1 $ t2) =
+    @{const HOL.disj} $ negate_term t1 $ negate_term t2
+  | negate_term (@{const HOL.disj} $ t1 $ t2) =
+    @{const HOL.conj} $ negate_term t1 $ negate_term t2
   | negate_term (@{const Not} $ t) = t
   | negate_term t = @{const Not} $ t
 
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -70,8 +70,8 @@
         do_quant bs AForall s T t'
       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
         do_quant bs AExists s T t'
-      | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
-      | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
+      | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
+      | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
       | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
       | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
         do_conn bs AIff t1 t2
@@ -125,8 +125,8 @@
             t0 $ Abs (s, T, aux (T :: Ts) t')
           | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
             aux Ts (t0 $ eta_expand Ts t1 1)
-          | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
-          | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+          | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+          | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
           | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
           | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
               $ t1 $ t2 =>
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/TFL/dcterm.ML
--- a/src/HOL/Tools/TFL/dcterm.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/TFL/dcterm.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -79,11 +79,11 @@
   in capply c (uncurry cabs r) end;
 
 
-local val c = mk_hol_const(@{const_name "op &"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+local val c = mk_hol_const(@{const_name HOL.conj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
 in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
 end;
 
-local val c = mk_hol_const(@{const_name "op |"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+local val c = mk_hol_const(@{const_name HOL.disj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
 in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
 end;
 
@@ -129,8 +129,8 @@
 val dest_pair   = dest_binop @{const_name Pair}
 val dest_eq     = dest_binop @{const_name "op ="}
 val dest_imp    = dest_binop @{const_name HOL.implies}
-val dest_conj   = dest_binop @{const_name "op &"}
-val dest_disj   = dest_binop @{const_name "op |"}
+val dest_conj   = dest_binop @{const_name HOL.conj}
+val dest_disj   = dest_binop @{const_name HOL.disj}
 val dest_select = dest_binder @{const_name Eps}
 val dest_exists = dest_binder @{const_name Ex}
 val dest_forall = dest_binder @{const_name All}
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/TFL/usyntax.ML
--- a/src/HOL/Tools/TFL/usyntax.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -183,12 +183,12 @@
 
 
 fun mk_conj{conj1,conj2} =
-   let val c = Const(@{const_name "op &"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+   let val c = Const(@{const_name HOL.conj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    in list_comb(c,[conj1,conj2])
    end;
 
 fun mk_disj{disj1,disj2} =
-   let val c = Const(@{const_name "op |"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+   let val c = Const(@{const_name HOL.disj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    in list_comb(c,[disj1,disj2])
    end;
 
@@ -259,10 +259,10 @@
 fun dest_neg(Const(@{const_name Not},_) $ M) = M
   | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
 
-fun dest_conj(Const(@{const_name "op &"},_) $ M $ N) = {conj1=M, conj2=N}
+fun dest_conj(Const(@{const_name HOL.conj},_) $ M $ N) = {conj1=M, conj2=N}
   | dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
 
-fun dest_disj(Const(@{const_name "op |"},_) $ M $ N) = {disj1=M, disj2=N}
+fun dest_disj(Const(@{const_name HOL.disj},_) $ M $ N) = {disj1=M, disj2=N}
   | dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
 
 fun mk_pair{fst,snd} =
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -95,8 +95,8 @@
 
 fun is_atom (Const (@{const_name False}, _))                                           = false
   | is_atom (Const (@{const_name True}, _))                                            = false
-  | is_atom (Const (@{const_name "op &"}, _) $ _ $ _)                                    = false
-  | is_atom (Const (@{const_name "op |"}, _) $ _ $ _)                                    = false
+  | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _)                                    = false
+  | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _)                                    = false
   | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _)                                  = false
   | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _)       = false
   | is_atom (Const (@{const_name Not}, _) $ _)                                         = false
@@ -105,7 +105,7 @@
 fun is_literal (Const (@{const_name Not}, _) $ x) = is_atom x
   | is_literal x                      = is_atom x;
 
-fun is_clause (Const (@{const_name "op |"}, _) $ x $ y) = is_clause x andalso is_clause y
+fun is_clause (Const (@{const_name HOL.disj}, _) $ x $ y) = is_clause x andalso is_clause y
   | is_clause x                           = is_literal x;
 
 (* ------------------------------------------------------------------------- *)
@@ -184,14 +184,14 @@
 
 (* Theory.theory -> Term.term -> Thm.thm *)
 
-fun make_nnf_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
+fun make_nnf_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
 	let
 		val thm1 = make_nnf_thm thy x
 		val thm2 = make_nnf_thm thy y
 	in
 		conj_cong OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
+  | make_nnf_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
 	let
 		val thm1 = make_nnf_thm thy x
 		val thm2 = make_nnf_thm thy y
@@ -218,14 +218,14 @@
 	make_nnf_not_false
   | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
 	make_nnf_not_true
-  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op &"}, _) $ x $ y)) =
+  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) =
 	let
 		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
 		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
 	in
 		make_nnf_not_conj OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op |"}, _) $ x $ y)) =
+  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.disj}, _) $ x $ y)) =
 	let
 		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
 		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
@@ -276,7 +276,7 @@
 
 (* Theory.theory -> Term.term -> Thm.thm *)
 
-fun simp_True_False_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
+fun simp_True_False_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
 	let
 		val thm1 = simp_True_False_thm thy x
 		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
@@ -298,7 +298,7 @@
 					conj_cong OF [thm1, thm2]  (* (x & y) = (x' & y') *)
 			end
 	end
-  | simp_True_False_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
+  | simp_True_False_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
 	let
 		val thm1 = simp_True_False_thm thy x
 		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
@@ -334,24 +334,24 @@
 fun make_cnf_thm thy t =
 let
 	(* Term.term -> Thm.thm *)
-	fun make_cnf_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) =
+	fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) =
 		let
 			val thm1 = make_cnf_thm_from_nnf x
 			val thm2 = make_cnf_thm_from_nnf y
 		in
 			conj_cong OF [thm1, thm2]
 		end
-	  | make_cnf_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
+	  | make_cnf_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
 		let
 			(* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
-			fun make_cnf_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
+			fun make_cnf_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
 				let
 					val thm1 = make_cnf_disj_thm x1 y'
 					val thm2 = make_cnf_disj_thm x2 y'
 				in
 					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
 				end
-			  | make_cnf_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
+			  | make_cnf_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
 				let
 					val thm1 = make_cnf_disj_thm x' y1
 					val thm2 = make_cnf_disj_thm x' y2
@@ -403,27 +403,27 @@
 	val var_id = Unsynchronized.ref 0  (* properly initialized below *)
 	fun new_free () =
 		Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
-	fun make_cnfx_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) : thm =
+	fun make_cnfx_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) : thm =
 		let
 			val thm1 = make_cnfx_thm_from_nnf x
 			val thm2 = make_cnfx_thm_from_nnf y
 		in
 			conj_cong OF [thm1, thm2]
 		end
-	  | make_cnfx_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
+	  | make_cnfx_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
 		if is_clause x andalso is_clause y then
 			inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
 		else if is_literal y orelse is_literal x then let
 			(* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
 			(* almost in CNF, and x' or y' is a literal                      *)
-			fun make_cnfx_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
+			fun make_cnfx_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
 				let
 					val thm1 = make_cnfx_disj_thm x1 y'
 					val thm2 = make_cnfx_disj_thm x2 y'
 				in
 					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
 				end
-			  | make_cnfx_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
+			  | make_cnfx_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
 				let
 					val thm1 = make_cnfx_disj_thm x' y1
 					val thm2 = make_cnfx_disj_thm x' y2
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/groebner.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -395,7 +395,7 @@
 
 fun refute_disj rfn tm =
  case term_of tm of
-  Const(@{const_name "op |"},_)$l$r =>
+  Const(@{const_name HOL.disj},_)$l$r =>
    compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE))
   | _ => rfn tm ;
 
@@ -454,7 +454,7 @@
 val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
 
 val cTrp = @{cterm "Trueprop"};
-val cConj = @{cterm "op &"};
+val cConj = @{cterm HOL.conj};
 val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"});
 val assume_Trueprop = mk_comb cTrp #> assume;
 val list_mk_conj = list_mk_binop cConj;
@@ -479,22 +479,22 @@
   (* FIXME : copied from cqe.ML -- complex QE*)
 fun conjuncts ct =
  case term_of ct of
-  @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
+  @{term HOL.conj}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
 | _ => [ct];
 
 fun fold1 f = foldr1 (uncurry f);
 
-val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ;
+val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm HOL.conj} c) c') ;
 
 fun mk_conj_tab th = 
  let fun h acc th = 
    case prop_of th of
-   @{term "Trueprop"}$(@{term "op &"}$p$q) => 
+   @{term "Trueprop"}$(@{term HOL.conj}$p$q) => 
      h (h acc (th RS conjunct2)) (th RS conjunct1)
   | @{term "Trueprop"}$p => (p,th)::acc
 in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
 
-fun is_conj (@{term "op &"}$_$_) = true
+fun is_conj (@{term HOL.conj}$_$_) = true
   | is_conj _ = false;
 
 fun prove_conj tab cjs = 
@@ -852,14 +852,14 @@
  fun unwind_polys_conv tm =
  let 
   val (vars,bod) = strip_exists tm
-  val cjs = striplist (dest_binary @{cterm "op &"}) bod
+  val cjs = striplist (dest_binary @{cterm HOL.conj}) bod
   val th1 = (the (get_first (try (isolate_variable vars)) cjs) 
              handle Option => raise CTERM ("unwind_polys_conv",[tm]))
   val eq = Thm.lhs_of th1
-  val bod' = list_mk_binop @{cterm "op &"} (eq::(remove op aconvc eq cjs))
+  val bod' = list_mk_binop @{cterm HOL.conj} (eq::(remove op aconvc eq cjs))
   val th2 = conj_ac_rule (mk_eq bod bod')
   val th3 = transitive th2 
-         (Drule.binop_cong_rule @{cterm "op &"} th1 
+         (Drule.binop_cong_rule @{cterm HOL.conj} th1 
                 (reflexive (Thm.dest_arg (Thm.rhs_of th2))))
   val v = Thm.dest_arg1(Thm.dest_arg1(Thm.rhs_of th3))
   val vars' = (remove op aconvc v vars) @ [v]
@@ -929,8 +929,8 @@
   | Const (@{const_name Not}, _) $ _ => find_term bounds (dest_arg tm)
   | Const (@{const_name All}, _) $ _ => find_body bounds (dest_arg tm)
   | Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm)
-  | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
-  | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
+  | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
+  | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
   | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
   | @{term "op ==>"} $_$_ => find_args bounds tm
   | Const("op ==",_)$_$_ => find_args bounds tm
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/hologic.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -208,8 +208,8 @@
   let val (th1, th2) = conj_elim th
   in conj_elims th1 @ conj_elims th2 end handle THM _ => [th];
 
-val conj = @{term "op &"}
-and disj = @{term "op |"}
+val conj = @{term HOL.conj}
+and disj = @{term HOL.disj}
 and imp = @{term implies}
 and Not = @{term Not};
 
@@ -218,14 +218,14 @@
 and mk_imp (t1, t2) = imp $ t1 $ t2
 and mk_not t = Not $ t;
 
-fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
+fun dest_conj (Const ("HOL.conj", _) $ t $ t') = t :: dest_conj t'
   | dest_conj t = [t];
 
-fun dest_disj (Const ("op |", _) $ t $ t') = t :: dest_disj t'
+fun dest_disj (Const ("HOL.disj", _) $ t $ t') = t :: dest_disj t'
   | dest_disj t = [t];
 
 (*Like dest_disj, but flattens disjunctions however nested*)
-fun disjuncts_aux (Const ("op |", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
+fun disjuncts_aux (Const ("HOL.disj", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
   | disjuncts_aux t disjs = t::disjs;
 
 fun disjuncts t = disjuncts_aux t [];
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -74,9 +74,9 @@
         in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
           (p (fold (Logic.all o Var) vs t) f)
         end;
-      fun mkop @{const_name "op &"} T x =
+      fun mkop @{const_name HOL.conj} T x =
             SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
-        | mkop @{const_name "op |"} T x =
+        | mkop @{const_name HOL.disj} T x =
             SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
         | mkop _ _ _ = NONE;
       fun mk_collect p T t =
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -46,7 +46,7 @@
 val mk_Trueprop = HOLogic.mk_Trueprop;
 
 fun atomize thm = case Thm.prop_of thm of
-    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
+    Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.conj}, _) $ _ $ _) =>
     atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
   | _ => [thm];
 
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -151,8 +151,8 @@
   let fun has (Const(a,_)) = false
         | has (Const(@{const_name Trueprop},_) $ p) = has p
         | has (Const(@{const_name Not},_) $ p) = has p
-        | has (Const(@{const_name "op |"},_) $ p $ q) = member (op =) bs @{const_name "op |"} orelse has p orelse has q
-        | has (Const(@{const_name "op &"},_) $ p $ q) = member (op =) bs @{const_name "op &"} orelse has p orelse has q
+        | has (Const(@{const_name HOL.disj},_) $ p $ q) = member (op =) bs @{const_name HOL.disj} orelse has p orelse has q
+        | has (Const(@{const_name HOL.conj},_) $ p $ q) = member (op =) bs @{const_name HOL.conj} orelse has p orelse has q
         | has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p
         | has (Const(@{const_name Ex},_) $ Abs(_,_,p)) = member (op =) bs @{const_name Ex} orelse has p
         | has _ = false
@@ -162,7 +162,7 @@
 (**** Clause handling ****)
 
 fun literals (Const(@{const_name Trueprop},_) $ P) = literals P
-  | literals (Const(@{const_name "op |"},_) $ P $ Q) = literals P @ literals Q
+  | literals (Const(@{const_name HOL.disj},_) $ P $ Q) = literals P @ literals Q
   | literals (Const(@{const_name Not},_) $ P) = [(false,P)]
   | literals P = [(true,P)];
 
@@ -172,7 +172,7 @@
 
 (*** Tautology Checking ***)
 
-fun signed_lits_aux (Const (@{const_name "op |"}, _) $ P $ Q) (poslits, neglits) =
+fun signed_lits_aux (Const (@{const_name HOL.disj}, _) $ P $ Q) (poslits, neglits) =
       signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
   | signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits)
   | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
@@ -208,16 +208,16 @@
 fun refl_clause_aux 0 th = th
   | refl_clause_aux n th =
        case HOLogic.dest_Trueprop (concl_of th) of
-          (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _) =>
+          (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) =>
             refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
-        | (Const (@{const_name "op |"}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
+        | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
             if eliminable(t,u)
             then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
             else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
-        | (Const (@{const_name "op |"}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
+        | (Const (@{const_name HOL.disj}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
         | _ => (*not a disjunction*) th;
 
-fun notequal_lits_count (Const (@{const_name "op |"}, _) $ P $ Q) =
+fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) =
       notequal_lits_count P + notequal_lits_count Q
   | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
   | notequal_lits_count _ = 0;
@@ -268,10 +268,10 @@
   (*Estimate the number of clauses in order to detect infeasible theorems*)
   fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t
     | signed_nclauses b (Const(@{const_name Not},_) $ t) = signed_nclauses (not b) t
-    | signed_nclauses b (Const(@{const_name "op &"},_) $ t $ u) =
+    | signed_nclauses b (Const(@{const_name HOL.conj},_) $ t $ u) =
         if b then sum (signed_nclauses b t) (signed_nclauses b u)
              else prod (signed_nclauses b t) (signed_nclauses b u)
-    | signed_nclauses b (Const(@{const_name "op |"},_) $ t $ u) =
+    | signed_nclauses b (Const(@{const_name HOL.disj},_) $ t $ u) =
         if b then prod (signed_nclauses b t) (signed_nclauses b u)
              else sum (signed_nclauses b t) (signed_nclauses b u)
     | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
@@ -330,10 +330,10 @@
   let val ctxtr = Unsynchronized.ref ctxt   (* FIXME ??? *)
       fun cnf_aux (th,ths) =
         if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
-        else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name "op &"}] (prop_of th))
+        else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th))
         then nodups ctxt th :: ths (*no work to do, terminate*)
         else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
-            Const (@{const_name "op &"}, _) => (*conjunction*)
+            Const (@{const_name HOL.conj}, _) => (*conjunction*)
                 cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
           | Const (@{const_name All}, _) => (*universal quantifier*)
                 let val (th',ctxt') = freeze_spec th (!ctxtr)
@@ -341,7 +341,7 @@
           | Const (@{const_name Ex}, _) =>
               (*existential quantifier: Insert Skolem functions*)
               cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
-          | Const (@{const_name "op |"}, _) =>
+          | Const (@{const_name HOL.disj}, _) =>
               (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
                 all combinations of converting P, Q to CNF.*)
               let val tac =
@@ -365,7 +365,7 @@
 (**** Generation of contrapositives ****)
 
 fun is_left (Const (@{const_name Trueprop}, _) $
-               (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _)) = true
+               (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _)) = true
   | is_left _ = false;
 
 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
@@ -400,7 +400,7 @@
 (*Is the string the name of a connective? Really only | and Not can remain,
   since this code expects to be called on a clause form.*)
 val is_conn = member (op =)
-    [@{const_name Trueprop}, @{const_name "op &"}, @{const_name "op |"},
+    [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
      @{const_name HOL.implies}, @{const_name Not},
      @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
 
@@ -429,7 +429,7 @@
 
 fun rigid t = not (is_Var (head_of t));
 
-fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name "op |"}, _) $ t $ _)) = rigid t
+fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t
   | ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t
   | ok4horn _ = false;
 
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/prop_logic.ML
--- a/src/HOL/Tools/prop_logic.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/prop_logic.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -397,14 +397,14 @@
 			(False, table)
 		  | aux (Const (@{const_name Not}, _) $ x)      table =
 			apfst Not (aux x table)
-		  | aux (Const (@{const_name "op |"}, _) $ x $ y) table =
+		  | aux (Const (@{const_name HOL.disj}, _) $ x $ y) table =
 			let
 				val (fm1, table1) = aux x table
 				val (fm2, table2) = aux y table1
 			in
 				(Or (fm1, fm2), table2)
 			end
-		  | aux (Const (@{const_name "op &"}, _) $ x $ y) table =
+		  | aux (Const (@{const_name HOL.conj}, _) $ x $ y) table =
 			let
 				val (fm1, table1) = aux x table
 				val (fm2, table2) = aux y table1
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -648,8 +648,8 @@
       | Const (@{const_name All}, _) => t
       | Const (@{const_name Ex}, _) => t
       | Const (@{const_name "op ="}, _) => t
-      | Const (@{const_name "op &"}, _) => t
-      | Const (@{const_name "op |"}, _) => t
+      | Const (@{const_name HOL.conj}, _) => t
+      | Const (@{const_name HOL.disj}, _) => t
       | Const (@{const_name HOL.implies}, _) => t
       (* sets *)
       | Const (@{const_name Collect}, _) => t
@@ -824,8 +824,8 @@
       | Const (@{const_name All}, T) => collect_type_axioms T axs
       | Const (@{const_name Ex}, T) => collect_type_axioms T axs
       | Const (@{const_name "op ="}, T) => collect_type_axioms T axs
-      | Const (@{const_name "op &"}, _) => axs
-      | Const (@{const_name "op |"}, _) => axs
+      | Const (@{const_name HOL.conj}, _) => axs
+      | Const (@{const_name HOL.disj}, _) => axs
       | Const (@{const_name HOL.implies}, _) => axs
       (* sets *)
       | Const (@{const_name Collect}, T) => collect_type_axioms T axs
@@ -1861,7 +1861,7 @@
       SOME (interpret thy model args (eta_expand t 1))
     | Const (@{const_name "op ="}, _) =>
       SOME (interpret thy model args (eta_expand t 2))
-    | Const (@{const_name "op &"}, _) $ t1 $ t2 =>
+    | Const (@{const_name HOL.conj}, _) $ t1 $ t2 =>
       (* 3-valued logic *)
       let
         val (i1, m1, a1) = interpret thy model args t1
@@ -1871,14 +1871,14 @@
       in
         SOME (Leaf [fmTrue, fmFalse], m2, a2)
       end
-    | Const (@{const_name "op &"}, _) $ t1 =>
+    | Const (@{const_name HOL.conj}, _) $ t1 =>
       SOME (interpret thy model args (eta_expand t 1))
-    | Const (@{const_name "op &"}, _) =>
+    | Const (@{const_name HOL.conj}, _) =>
       SOME (interpret thy model args (eta_expand t 2))
       (* this would make "undef" propagate, even for formulae like *)
       (* "False & undef":                                          *)
       (* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *)
-    | Const (@{const_name "op |"}, _) $ t1 $ t2 =>
+    | Const (@{const_name HOL.disj}, _) $ t1 $ t2 =>
       (* 3-valued logic *)
       let
         val (i1, m1, a1) = interpret thy model args t1
@@ -1888,9 +1888,9 @@
       in
         SOME (Leaf [fmTrue, fmFalse], m2, a2)
       end
-    | Const (@{const_name "op |"}, _) $ t1 =>
+    | Const (@{const_name HOL.disj}, _) $ t1 =>
       SOME (interpret thy model args (eta_expand t 1))
-    | Const (@{const_name "op |"}, _) =>
+    | Const (@{const_name HOL.disj}, _) =>
       SOME (interpret thy model args (eta_expand t 2))
       (* this would make "undef" propagate, even for formulae like *)
       (* "True | undef":                                           *)
diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -12,7 +12,7 @@
   (*abstract syntax*)
   fun dest_eq ((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME (c, s, t)
     | dest_eq _ = NONE;
-  fun dest_conj ((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME (c, s, t)
+  fun dest_conj ((c as Const(@{const_name HOL.conj},_)) $ s $ t) = SOME (c, s, t)
     | dest_conj _ = NONE;
   fun dest_imp ((c as Const(@{const_name HOL.implies},_)) $ s $ t) = SOME (c, s, t)
     | dest_imp _ = NONE;
@@ -160,7 +160,7 @@
 
 val mksimps_pairs =
  [(@{const_name HOL.implies}, [@{thm mp}]),
-  (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+  (@{const_name HOL.conj}, [@{thm conjunct1}, @{thm conjunct2}]),
   (@{const_name All}, [@{thm spec}]),
   (@{const_name True}, []),
   (@{const_name False}, []),
diff -r 2d638e963357 -r 848be46708dc src/HOL/ex/SVC_Oracle.thy
--- a/src/HOL/ex/SVC_Oracle.thy	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy	Fri Aug 27 10:56:46 2010 +0200
@@ -88,8 +88,8 @@
             else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
             else replace (c $ x $ y)   (*non-numeric comparison*)
     (*abstraction of a formula*)
-    and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
-      | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+    and fm ((c as Const(@{const_name HOL.conj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+      | fm ((c as Const(@{const_name HOL.disj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
       | fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q)
       | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
       | fm ((c as Const(@{const_name True}, _))) = c
diff -r 2d638e963357 -r 848be46708dc src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -89,8 +89,8 @@
    let fun tag t =
          let val (c,ts) = strip_comb t
          in  case c of
-             Const(@{const_name "op &"}, _)   => apply c (map tag ts)
-           | Const(@{const_name "op |"}, _)   => apply c (map tag ts)
+             Const(@{const_name HOL.conj}, _)   => apply c (map tag ts)
+           | Const(@{const_name HOL.disj}, _)   => apply c (map tag ts)
            | Const(@{const_name HOL.implies}, _) => apply c (map tag ts)
            | Const(@{const_name Not}, _)    => apply c (map tag ts)
            | Const(@{const_name True}, _)   => (c, false)
@@ -183,9 +183,9 @@
       | tm t = Int (lit t)
                handle Match => var (t,[])
     (*translation of a formula*)
-    and fm pos (Const(@{const_name "op &"}, _) $ p $ q) =
+    and fm pos (Const(@{const_name HOL.conj}, _) $ p $ q) =
             Buildin("AND", [fm pos p, fm pos q])
-      | fm pos (Const(@{const_name "op |"}, _) $ p $ q) =
+      | fm pos (Const(@{const_name HOL.disj}, _) $ p $ q) =
             Buildin("OR", [fm pos p, fm pos q])
       | fm pos (Const(@{const_name HOL.implies}, _) $ p $ q) =
             Buildin("=>", [fm (not pos) p, fm pos q])
diff -r 2d638e963357 -r 848be46708dc src/HOLCF/Tools/Domain/domain_library.ML
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -121,7 +121,7 @@
       val r_inst = read_instantiate ctxt;
       fun at thm =
           case concl_of thm of
-            _$(Const(@{const_name "op &"},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
+            _$(Const(@{const_name HOL.conj},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
           | _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
           | _                             => [thm];
     in map zero_var_indexes (at thm) end;
diff -r 2d638e963357 -r 848be46708dc src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -271,9 +271,6 @@
        of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
         | NONE => Codegen.thyname_of_const thy c);
   fun purify_base "==>" = "follows"
-    | purify_base "op &" = "and"
-    | purify_base "op |" = "or"
-    | purify_base "op -->" = "implies"
     | purify_base "op =" = "eq"
     | purify_base s = Name.desymbolize false s;
   fun namify thy get_basename get_thyname name =