# HG changeset patch
# User haftmann
# Date 1283153730 -7200
# Node ID 43c934dd4bc38d55f3e16ed4499356c9f54bd108
# Parent  9070a7c356c96c4ebebb75f8e11d163679edb435# Parent  4abe644fcea505c8834863dc95952dfab228c28e
merged

diff -r 9070a7c356c9 -r 43c934dd4bc3 NEWS
--- a/NEWS	Mon Aug 30 09:28:02 2010 +0200
+++ b/NEWS	Mon Aug 30 09:35:30 2010 +0200
@@ -136,6 +136,7 @@
     op & ~> HOL.conj
     op | ~> HOL.disj
     op --> ~> HOL.implies
+    op = ~> HOL.eq
     Not ~> HOL.Not
     The ~> HOL.The
     All ~> HOL.All
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Aug 30 09:35:30 2010 +0200
@@ -3305,7 +3305,7 @@
                              (Const (@{const_name Set.member}, _) $
                               Free (name, _) $ _)) = name
         | variable_of_bound (Const (@{const_name Trueprop}, _) $
-                             (Const (@{const_name "op ="}, _) $
+                             (Const (@{const_name HOL.eq}, _) $
                               Free (name, _) $ _)) = name
         | variable_of_bound t = raise TERM ("variable_of_bound", [t])
 
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Aug 30 09:35:30 2010 +0200
@@ -519,9 +519,9 @@
   val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
   fun h x t =
    case term_of t of
-     Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
+     Const(@{const_name HOL.eq}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
                             else Ferrante_Rackoff_Data.Nox
-   | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
+   | @{term "Not"}$(Const(@{const_name HOL.eq}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
                             else Ferrante_Rackoff_Data.Nox
    | b$y$z => if Term.could_unify (b, lt) then
                  if term_of x aconv y then Ferrante_Rackoff_Data.Lt
@@ -771,7 +771,7 @@
       in rth end
     | _ => Thm.reflexive ct)
 
-|  Const(@{const_name "op ="},_)$_$Const(@{const_name Groups.zero},_) =>
+|  Const(@{const_name HOL.eq},_)$_$Const(@{const_name Groups.zero},_) =>
    (case whatis x (Thm.dest_arg1 ct) of
     ("c*x+t",[c,t]) =>
        let
@@ -835,7 +835,7 @@
        val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
 
-| Const(@{const_name "op ="},_)$a$b =>
+| Const(@{const_name HOL.eq},_)$a$b =>
    let val (ca,cb) = Thm.dest_binop ct
        val T = ctyp_of_term ca
        val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
@@ -844,7 +844,7 @@
               (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
        val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
-| @{term "Not"} $(Const(@{const_name "op ="},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
+| @{term "Not"} $(Const(@{const_name HOL.eq},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
 | _ => Thm.reflexive ct
 end;
 
@@ -852,9 +852,9 @@
  let
   fun h x t =
    case term_of t of
-     Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
+     Const(@{const_name HOL.eq}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
                             else Ferrante_Rackoff_Data.Nox
-   | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
+   | @{term "Not"}$(Const(@{const_name HOL.eq}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
                             else Ferrante_Rackoff_Data.Nox
    | Const(@{const_name Orderings.less},_)$y$z =>
        if term_of x aconv y then Ferrante_Rackoff_Data.Lt
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Aug 30 09:35:30 2010 +0200
@@ -912,7 +912,7 @@
 
 definition "lt p = (case p of CP (C c) \<Rightarrow> if 0>\<^sub>N c then T else F| _ \<Rightarrow> Lt p)"
 definition "le p = (case p of CP (C c) \<Rightarrow> if 0\<ge>\<^sub>N c then T else F | _ \<Rightarrow> Le p)"
-definition "eq p = (case p of CP (C c) \<Rightarrow> if c = 0\<^sub>N then T else F | _ \<Rightarrow> Eq p)"
+definition eq where "eq p = (case p of CP (C c) \<Rightarrow> if c = 0\<^sub>N then T else F | _ \<Rightarrow> Eq p)"
 definition "neq p = not (eq p)"
 
 lemma lt: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (lt p) = Ifm vs bs (Lt p)"
@@ -2960,7 +2960,7 @@
 val ifft = @{term "op = :: bool => _"}
 fun llt rT = Const(@{const_name Orderings.less},rrT rT);
 fun lle rT = Const(@{const_name Orderings.less},rrT rT);
-fun eqt rT = Const(@{const_name "op ="},rrT rT);
+fun eqt rT = Const(@{const_name HOL.eq},rrT rT);
 fun rz rT = Const(@{const_name Groups.zero},rT);
 
 fun dest_nat t = case t of
@@ -3021,7 +3021,7 @@
   | 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 => 
+  | Const(@{const_name HOL.eq},ty)$p$q => 
        if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
        else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
   | Const(@{const_name Orderings.less},_)$p$q => 
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Decision_Procs/commutative_ring_tac.ML
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -65,7 +65,7 @@
 (* reification of the equation *)
 val cr_sort = @{sort "comm_ring_1"};
 
-fun reif_eq thy (eq as Const(@{const_name "op ="}, Type("fun", [T, _])) $ lhs $ rhs) =
+fun reif_eq thy (eq as Const(@{const_name HOL.eq}, Type("fun", [T, _])) $ lhs $ rhs) =
       if Sign.of_sort thy (T, cr_sort) then
         let
           val fs = OldTerm.term_frees eq;
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Decision_Procs/ferrante_rackoff.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -175,7 +175,7 @@
  let
   fun h bounds tm =
    (case term_of tm of
-     Const (@{const_name "op ="}, T) $ _ $ _ =>
+     Const (@{const_name HOL.eq}, T) $ _ $ _ =>
        if domain_type T = HOLogic.boolT then find_args bounds tm
        else Thm.dest_fun2 tm
    | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -116,7 +116,7 @@
 fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
 
 fun is_eqx x eq = case term_of eq of
-   Const(@{const_name "op ="},_)$l$r => l aconv term_of x orelse r aconv term_of x
+   Const(@{const_name HOL.eq},_)$l$r => l aconv term_of x orelse r aconv term_of x
  | _ => false ;
 
 local 
@@ -176,7 +176,7 @@
  let
   fun h bounds tm =
    (case term_of tm of
-     Const (@{const_name "op ="}, T) $ _ $ _ =>
+     Const (@{const_name HOL.eq}, T) $ _ $ _ =>
        if domain_type T = HOLogic.boolT then find_args bounds tm
        else Thm.dest_fun2 tm
    | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/HOL.thy	Mon Aug 30 09:35:30 2010 +0200
@@ -61,14 +61,8 @@
   disj          :: "[bool, bool] => bool"           (infixr "|" 30)
   implies       :: "[bool, bool] => bool"           (infixr "-->" 25)
 
-setup Sign.root_path
+  eq            :: "['a, 'a] => bool"               (infixl "=" 50)
 
-consts
-  "op ="        :: "['a, 'a] => bool"               (infixl "=" 50)
-
-setup Sign.local_path
-
-consts
   The           :: "('a => bool) => 'a"
   All           :: "('a => bool) => bool"           (binder "ALL " 10)
   Ex            :: "('a => bool) => bool"           (binder "EX " 10)
@@ -78,7 +72,7 @@
 subsubsection {* Additional concrete syntax *}
 
 notation (output)
-  "op ="  (infix "=" 50)
+  eq  (infix "=" 50)
 
 abbreviation
   not_equal :: "['a, 'a] => bool"  (infixl "~=" 50) where
@@ -89,15 +83,15 @@
 
 notation (xsymbols)
   Not  ("\<not> _" [40] 40) and
-  HOL.conj  (infixr "\<and>" 35) and
-  HOL.disj  (infixr "\<or>" 30) and
-  HOL.implies  (infixr "\<longrightarrow>" 25) and
+  conj  (infixr "\<and>" 35) and
+  disj  (infixr "\<or>" 30) and
+  implies  (infixr "\<longrightarrow>" 25) and
   not_equal  (infix "\<noteq>" 50)
 
 notation (HTML output)
   Not  ("\<not> _" [40] 40) and
-  HOL.conj  (infixr "\<and>" 35) and
-  HOL.disj  (infixr "\<or>" 30) and
+  conj  (infixr "\<and>" 35) and
+  disj  (infixr "\<or>" 30) and
   not_equal  (infix "\<noteq>" 50)
 
 abbreviation (iff)
@@ -183,8 +177,8 @@
   True_or_False:  "(P=True) | (P=False)"
 
 finalconsts
-  "op ="
-  HOL.implies
+  eq
+  implies
   The
 
 definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where
@@ -864,7 +858,7 @@
 
 setup {*
 let
-  fun non_bool_eq (@{const_name "op ="}, Type (_, [T, _])) = T <> @{typ bool}
+  fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
     | non_bool_eq _ = false;
   val hyp_subst_tac' =
     SUBGOAL (fn (goal, i) =>
@@ -930,7 +924,7 @@
 (
   val thy = @{theory}
   type claset = Classical.claset
-  val equality_name = @{const_name "op ="}
+  val equality_name = @{const_name HOL.eq}
   val not_name = @{const_name Not}
   val notE = @{thm notE}
   val ccontr = @{thm ccontr}
@@ -1746,8 +1740,8 @@
 
 fun eq_codegen thy defs dep thyname b t gr =
     (case strip_comb t of
-       (Const (@{const_name "op ="}, Type (_, [Type ("fun", _), _])), _) => NONE
-     | (Const (@{const_name "op ="}, _), [t, u]) =>
+       (Const (@{const_name HOL.eq}, Type (_, [Type ("fun", _), _])), _) => NONE
+     | (Const (@{const_name HOL.eq}, _), [t, u]) =>
           let
             val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
             val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
@@ -1756,7 +1750,7 @@
             SOME (Codegen.parens
               (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
           end
-     | (t as Const (@{const_name "op ="}, _), ts) => SOME (Codegen.invoke_codegen
+     | (t as Const (@{const_name HOL.eq}, _), ts) => SOME (Codegen.invoke_codegen
          thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
      | _ => NONE);
 
@@ -1796,7 +1790,7 @@
 
 setup {*
   Code_Preproc.map_pre (fn simpset =>
-    simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term "op ="}]
+    simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}]
       (fn thy => fn _ => fn Const (_, T) => case strip_type T
         of (Type _ :: _, _) => SOME @{thm eq_equal}
          | _ => NONE)])
@@ -1944,7 +1938,7 @@
 code_const "HOL.equal"
   (Haskell infixl 4 "==")
 
-code_const "op ="
+code_const HOL.eq
   (Haskell infixl 4 "==")
 
 text {* undefined *}
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Mon Aug 30 09:35:30 2010 +0200
@@ -53,7 +53,7 @@
   F > False
   ONE_ONE > HOL4Setup.ONE_ONE
   ONTO    > Fun.surj
-  "=" > "op ="
+  "=" > HOL.eq
   "==>" > HOL.implies
   "/\\" > HOL.conj
   "\\/" > HOL.disj
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Import/HOLLight/hollight.imp
--- a/src/HOL/Import/HOLLight/hollight.imp	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp	Mon Aug 30 09:35:30 2010 +0200
@@ -234,7 +234,7 @@
   ">=" > "HOLLight.hollight.>="
   ">" > "HOLLight.hollight.>"
   "==>" > HOL.implies
-  "=" > "op ="
+  "=" > HOL.eq
   "<=" > "HOLLight.hollight.<="
   "<" > "HOLLight.hollight.<"
   "/\\" > HOL.conj
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Import/hol4rews.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -627,7 +627,7 @@
         thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool}
             |> add_hol4_type_mapping "min" "fun" false "fun"
             |> add_hol4_type_mapping "min" "ind" false @{type_name ind}
-            |> add_hol4_const_mapping "min" "=" false @{const_name "op ="}
+            |> add_hol4_const_mapping "min" "=" false @{const_name HOL.eq}
             |> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies}
             |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
 in
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Mon Aug 30 09:35:30 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 HOL.conj} orelse c = @{const_name "op ="}
+        orelse c = @{const_name HOL.implies} orelse c = @{const_name HOL.conj} orelse c = @{const_name HOL.eq}
       then I else insert (op =) c
     | _ => I) t [];
 
@@ -1213,7 +1213,7 @@
     let
         fun add_consts (Const (c, _), cs) =
             (case c of
-                 @{const_name "op ="} => insert (op =) "==" cs
+                 @{const_name HOL.eq} => insert (op =) "==" cs
                | @{const_name HOL.implies} => insert (op =) "==>" cs
                | @{const_name All} => cs
                | "all" => cs
@@ -1476,10 +1476,10 @@
 fun mk_COMB th1 th2 thy =
     let
         val (f,g) = case concl_of th1 of
-                        _ $ (Const(@{const_name "op ="},_) $ f $ g) => (f,g)
+                        _ $ (Const(@{const_name HOL.eq},_) $ f $ g) => (f,g)
                       | _ => raise ERR "mk_COMB" "First theorem not an equality"
         val (x,y) = case concl_of th2 of
-                        _ $ (Const(@{const_name "op ="},_) $ x $ y) => (x,y)
+                        _ $ (Const(@{const_name HOL.eq},_) $ x $ y) => (x,y)
                       | _ => raise ERR "mk_COMB" "Second theorem not an equality"
         val fty = type_of f
         val (fd,fr) = dom_rng fty
@@ -1788,7 +1788,7 @@
         val cv = cterm_of thy v
         val th1 = implies_elim_all (beta_eta_thm th)
         val (f,g) = case concl_of th1 of
-                        _ $ (Const(@{const_name "op ="},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
+                        _ $ (Const(@{const_name HOL.eq},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
                       | _ => raise ERR "mk_ABS" "Bad conclusion"
         val (fd,fr) = dom_rng (type_of f)
         val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Import/shuffler.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -60,14 +60,14 @@
 
 fun mk_meta_eq th =
     (case concl_of th of
-         Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th RS eq_reflection
+         Const(@{const_name Trueprop},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _) => th RS eq_reflection
        | Const("==",_) $ _ $ _ => th
        | _ => raise THM("Not an equality",0,[th]))
     handle _ => raise THM("Couldn't make meta equality",0,[th])  (* FIXME avoid handle _ *)
 
 fun mk_obj_eq th =
     (case concl_of th of
-         Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th
+         Const(@{const_name Trueprop},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _) => th
        | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
        | _ => raise THM("Not an equality",0,[th]))
     handle _ => raise THM("Couldn't make object equality",0,[th])  (* FIXME avoid handle _ *)
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Library/OptionalSugar.thy	Mon Aug 30 09:35:30 2010 +0200
@@ -32,7 +32,7 @@
 (* deprecated, use thm with style instead, will be removed *)
 (* aligning equations *)
 notation (tab output)
-  "op ="  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
+  "HOL.eq"  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
   "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
 
 (* Let *)
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Library/reflection.ML
--- a/src/HOL/Library/reflection.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Library/reflection.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -82,7 +82,7 @@
 fun rearrange congs =
   let
     fun P (_, th) =
-      let val @{term "Trueprop"}$(Const (@{const_name "op ="},_) $l$_) = concl_of th
+      let val @{term "Trueprop"}$(Const (@{const_name HOL.eq},_) $l$_) = concl_of th
       in can dest_Var l end
     val (yes,no) = List.partition P congs
   in no @ yes end
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Mutabelle/Mutabelle.thy
--- a/src/HOL/Mutabelle/Mutabelle.thy	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Mutabelle/Mutabelle.thy	Mon Aug 30 09:35:30 2010 +0200
@@ -4,7 +4,7 @@
 begin
 
 ML {*
-val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}];
+val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}];
 
 val forbidden =
  [(@{const_name Power.power}, "'a"),
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -187,7 +187,7 @@
 val nitpick_mtd = ("nitpick", invoke_nitpick)
 *)
 
-val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}]
+val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]
 
 val forbidden =
  [(* (@{const_name "power"}, "'a"), *)
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -183,7 +183,7 @@
   end;
 
 fun mk_not_sym ths = maps (fn th => case prop_of th of
-    _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) => [th, th RS not_sym]
+    _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) => [th, th RS not_sym]
   | _ => [th]) ths;
 
 fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -147,7 +147,7 @@
              else raise EQVT_FORM "Type Implication"
           end
        (* case: eqvt-lemma is of the equational form *)
-      | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $
+      | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $
             (Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
            (if (apply_pi lhs (pi,typi)) = rhs
                then [orig_thm]
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Set.thy	Mon Aug 30 09:35:30 2010 +0200
@@ -268,7 +268,7 @@
 
     fun setcompr_tr [e, idts, b] =
       let
-        val eq = Syntax.const @{const_syntax "op ="} $ Bound (nvars idts) $ e;
+        val eq = Syntax.const @{const_syntax HOL.eq} $ Bound (nvars idts) $ e;
         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;
@@ -289,7 +289,7 @@
     let
       fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
         | check (Const (@{const_syntax HOL.conj}, _) $
-              (Const (@{const_syntax "op ="}, _) $ Bound m $ e) $ P, n) =
+              (Const (@{const_syntax HOL.eq}, _) $ 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, []))
         | check _ = false;
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Statespace/distinct_tree_prover.ML
--- a/src/HOL/Statespace/distinct_tree_prover.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -343,7 +343,7 @@
   end handle Option => NONE)
 
 fun distinctTree_tac names ctxt 
-      (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ x $ y)), i) =
+      (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ x $ y)), i) =
   (case get_fst_success (neq_x_y ctxt x y) names of
      SOME neq => rtac neq i
    | NONE => no_tac)
@@ -356,7 +356,7 @@
 
 fun distinct_simproc names =
   Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
-    (fn thy => fn ss => fn (Const (@{const_name "op ="},_)$x$y) =>
+    (fn thy => fn ss => fn (Const (@{const_name HOL.eq},_)$x$y) =>
         case try Simplifier.the_context ss of
         SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq]) 
                       (get_fst_success (neq_x_y ctxt x y) names)
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -285,7 +285,7 @@
                             then Bound 2
                             else raise TERM ("",[n]);
                    val sel' = lo $ d $ n' $ s;
-                  in (Const (@{const_name "op ="},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
+                  in (Const (@{const_name HOL.eq},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
 
          fun dest_state (s as Bound 0) = s
            | dest_state (s as (Const (sel,sT)$Bound 0)) =
@@ -295,10 +295,10 @@
            | dest_state s = 
                     raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s]);
   
-         fun dest_sel_eq (Const (@{const_name "op ="},Teq)$
+         fun dest_sel_eq (Const (@{const_name HOL.eq},Teq)$
                            ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)$X) =
                            (false,Teq,lT,lo,d,n,X,dest_state s)
-           | dest_sel_eq (Const (@{const_name "op ="},Teq)$X$
+           | dest_sel_eq (Const (@{const_name HOL.eq},Teq)$X$
                             ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)) =
                            (true,Teq,lT,lo,d,n,X,dest_state s)
            | dest_sel_eq _ = raise TERM ("",[]);
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -223,7 +223,7 @@
 
 fun distinctTree_tac ctxt
       (Const (@{const_name Trueprop},_) $
-        (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) =
+        (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ (x as Free _)$ (y as Free _))), i) =
   (case (neq_x_y ctxt x y) of
      SOME neq => rtac neq i
    | NONE => no_tac)
@@ -236,7 +236,7 @@
 
 val distinct_simproc =
   Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
-    (fn thy => fn ss => (fn (Const (@{const_name "op ="},_)$(x as Free _)$(y as Free _)) =>
+    (fn thy => fn ss => (fn (Const (@{const_name HOL.eq},_)$(x as Free _)$(y as Free _)) =>
         (case try Simplifier.the_context ss of
           SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
                        (neq_x_y ctxt x y)
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -416,7 +416,7 @@
     fun prove_case_cong ((t, nchotomy), case_rewrites) =
       let
         val (Const ("==>", _) $ tm $ _) = t;
-        val (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ Ma)) = tm;
+        val (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma)) = tm;
         val cert = cterm_of thy;
         val nchotomy' = nchotomy RS spec;
         val [v] = Term.add_vars (concl_of nchotomy') [];
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -96,7 +96,7 @@
         fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
           $ Free ("x", ty) $ Free ("y", ty);
         val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
-          (mk_side @{const_name HOL.equal}, mk_side @{const_name "op ="}));
+          (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq}));
         val def' = Syntax.check_term lthy def;
         val ((_, (_, thm)), lthy') = Specification.definition
           (NONE, (Attrib.empty_binding, def')) lthy;
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Mon Aug 30 09:35:30 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 HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
+        val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ (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 HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
+    val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ (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 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Nitpick/minipick.ML
--- a/src/HOL/Tools/Nitpick/minipick.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -123,7 +123,7 @@
          Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')
        | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
          to_F Ts (t0 $ eta_expand Ts t1 1)
-       | Const (@{const_name "op ="}, _) $ t1 $ t2 =>
+       | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
          RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
        | Const (@{const_name ord_class.less_eq},
                 Type (@{type_name fun},
@@ -165,8 +165,8 @@
          @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
        | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
        | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
-       | Const (@{const_name "op ="}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
-       | Const (@{const_name "op ="}, _) => to_R_rep Ts (eta_expand Ts t 2)
+       | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
+       | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
        | Const (@{const_name ord_class.less_eq},
                 Type (@{type_name fun},
                       [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -408,7 +408,7 @@
    (@{const_name True}, 0),
    (@{const_name All}, 1),
    (@{const_name Ex}, 1),
-   (@{const_name "op ="}, 1),
+   (@{const_name HOL.eq}, 1),
    (@{const_name HOL.conj}, 2),
    (@{const_name HOL.disj}, 2),
    (@{const_name HOL.implies}, 2),
@@ -1275,7 +1275,7 @@
         forall is_Var args andalso not (has_duplicates (op =) args)
       | _ => false
     fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
-      | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
+      | do_eq (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)) =
         do_lhs t1
       | do_eq _ = false
   in do_eq end
@@ -1347,7 +1347,7 @@
     @{const "==>"} $ _ $ t2 => term_under_def t2
   | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
   | @{const Trueprop} $ t1 => term_under_def t1
-  | Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1
+  | Const (@{const_name HOL.eq}, _) $ t1 $ _ => term_under_def t1
   | Abs (_, _, t') => term_under_def t'
   | t1 $ _ => term_under_def t1
   | _ => t
@@ -1371,7 +1371,7 @@
     val (lhs, rhs) =
       case t of
         Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
-      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
+      | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =>
         (t1, t2)
       | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
     val args = strip_comb lhs |> snd
@@ -1453,7 +1453,7 @@
   | @{const "==>"} $ _ $ t2 => lhs_of_equation t2
   | @{const Trueprop} $ t1 => lhs_of_equation t1
   | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
-  | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
+  | Const (@{const_name HOL.eq}, _) $ t1 $ _ => SOME t1
   | @{const HOL.implies} $ _ $ t2 => lhs_of_equation t2
   | _ => NONE
 fun is_constr_pattern _ (Bound _) = true
@@ -1807,7 +1807,7 @@
                         (betapply (t2, var_t))
     end
   | extensional_equal _ T t1 t2 =
-    Const (@{const_name "op ="}, T --> T --> bool_T) $ t1 $ t2
+    Const (@{const_name HOL.eq}, T --> T --> bool_T) $ t1 $ t2
 
 fun equationalize_term ctxt tag t =
   let
@@ -1816,7 +1816,7 @@
   in
     Logic.list_implies (prems,
         case concl of
-          @{const Trueprop} $ (Const (@{const_name "op ="}, Type (_, [T, _]))
+          @{const Trueprop} $ (Const (@{const_name HOL.eq}, Type (_, [T, _]))
                                $ t1 $ t2) =>
           @{const Trueprop} $ extensional_equal j T t1 t2
         | @{const Trueprop} $ t' =>
@@ -2290,7 +2290,7 @@
   | simps => simps
 fun is_equational_fun_surely_complete hol_ctxt x =
   case equational_fun_axioms hol_ctxt x of
-    [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
+    [@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)] =>
     strip_comb t1 |> snd |> forall is_Var
   | _ => false
 
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -590,7 +590,7 @@
                       if co then
                         Const (@{const_name The}, (T --> bool_T) --> T)
                         $ Abs (cyclic_co_val_name (), T,
-                               Const (@{const_name "op ="}, T --> T --> bool_T)
+                               Const (@{const_name HOL.eq}, T --> T --> bool_T)
                                $ Bound 0 $ abstract_over (var, t))
                       else
                         cyclic_atom ()
@@ -849,7 +849,7 @@
 (** Model reconstruction **)
 
 fun unfold_outer_the_binders (t as Const (@{const_name The}, _)
-                                   $ Abs (s, T, Const (@{const_name "op ="}, _)
+                                   $ Abs (s, T, Const (@{const_name HOL.eq}, _)
                                                 $ Bound 0 $ t')) =
     betapply (Abs (s, T, t'), t) |> unfold_outer_the_binders
   | unfold_outer_the_binders t = t
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -222,7 +222,7 @@
   | fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
   | fin_fun_body dom_T ran_T
                  ((t0 as Const (@{const_name If}, _))
-                  $ (t1 as Const (@{const_name "op ="}, _) $ Bound 0 $ t1')
+                  $ (t1 as Const (@{const_name HOL.eq}, _) $ Bound 0 $ t1')
                   $ t2 $ t3) =
     (if loose_bvar1 (t1', 0) then
        NONE
@@ -650,7 +650,7 @@
                                      Bound 0)))) accum
                   |>> mtype_of_mterm
                 end
-              | @{const_name "op ="} => do_equals T accum
+              | @{const_name HOL.eq} => do_equals T accum
               | @{const_name The} =>
                 (trace_msg (K "*** The"); raise UNSOLVABLE ())
               | @{const_name Eps} =>
@@ -760,7 +760,7 @@
                     do_term (incr_boundvars ~1 t1') accum
                   else
                     raise SAME ()
-                | (t11 as Const (@{const_name "op ="}, _)) $ Bound 0 $ t13 =>
+                | (t11 as Const (@{const_name HOL.eq}, _)) $ Bound 0 $ t13 =>
                   if not (loose_bvar1 (t13, 0)) then
                     do_term (incr_boundvars ~1 (t11 $ t13)) accum
                   else
@@ -876,7 +876,7 @@
                 do_term (@{const Not}
                          $ (HOLogic.eq_const (domain_type T0) $ t1
                             $ Abs (Name.uu, T1, @{const False}))) accum)
-           | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
+           | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
              do_equals x t1 t2
            | Const (@{const_name Let}, _) $ t1 $ t2 =>
              do_formula sn (betapply (t2, t1)) accum
@@ -973,7 +973,7 @@
             do_conjunction t0 t1 t2 accum
           | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
             do_all t0 s0 T1 t1 accum
-          | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
+          | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
             consider_general_equals mdata true x 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
@@ -1069,7 +1069,7 @@
                     Abs (Name.uu, set_T', @{const True})
                   | _ => Const (s, T')
                 else if s = @{const_name "=="} orelse
-                        s = @{const_name "op ="} then
+                        s = @{const_name HOL.eq} then
                   let
                     val T =
                       case T' of
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -447,7 +447,7 @@
                 val t1 = incr_boundvars n t1
                 val t2 = incr_boundvars n t2
                 val xs = map Bound (n - 1 downto 0)
-                val equation = Const (@{const_name "op ="},
+                val equation = Const (@{const_name HOL.eq},
                                       body_T --> body_T --> bool_T)
                                    $ betapplys (t1, xs) $ betapplys (t2, xs)
                 val t =
@@ -515,9 +515,9 @@
           do_description_operator The @{const_name undefined_fast_The} x t1
         | (Const (x as (@{const_name Eps}, _)), [t1]) =>
           do_description_operator Eps @{const_name undefined_fast_Eps} x t1
-        | (Const (@{const_name "op ="}, T), [t1]) =>
+        | (Const (@{const_name HOL.eq}, 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 HOL.eq}, T), [t1, t2]) => sub_equals T t1 t2
         | (Const (@{const_name HOL.conj}, _), [t1, t2]) =>
           Op2 (And, bool_T, Any, sub' t1, sub' t2)
         | (Const (@{const_name HOL.disj}, _), [t1, t2]) =>
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -41,7 +41,7 @@
     fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) =
         aux def t1 andalso aux false t2
       | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
-      | aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) =
+      | aux def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
         aux def t1 andalso aux false t2
       | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
       | aux def (t1 $ t2) = aux def t1 andalso aux def t2
@@ -149,7 +149,7 @@
       case t of
         @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
       | Const (s0, _) $ t1 $ _ =>
-        if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
+        if s0 = @{const_name "=="} orelse s0 = @{const_name HOL.eq} then
           let
             val (t', args) = strip_comb t1
             val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
@@ -209,7 +209,7 @@
         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
       | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
-      | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
+      | Const (s0 as @{const_name HOL.eq}, T0) $ t1 $ t2 =>
         do_equals new_Ts old_Ts s0 T0 t1 t2
       | @{const HOL.conj} $ t1 $ t2 =>
         @{const HOL.conj} $ do_term new_Ts old_Ts polar t1
@@ -332,7 +332,7 @@
         do_eq_or_imp Ts true def t0 t1 t2 seen
       | (t0 as @{const "==>"}) $ t1 $ t2 =>
         if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
-      | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
+      | (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
         do_eq_or_imp Ts true def t0 t1 t2 seen
       | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
         do_eq_or_imp Ts false def t0 t1 t2 seen
@@ -399,7 +399,7 @@
         aux_eq careful true t0 t1 t2
       | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
         t0 $ aux false t1 $ aux careful t2
-      | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
+      | aux careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
         aux_eq careful true t0 t1 t2
       | aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
         t0 $ aux false t1 $ aux careful t2
@@ -464,9 +464,9 @@
     and aux_implies prems zs t1 t2 =
       case t1 of
         Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
-      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
+      | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Var z $ t') =>
         aux_eq prems zs z t' t1 t2
-      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
+      | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t' $ Var z) =>
         aux_eq prems zs z t' t1 t2
       | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
     and aux_eq prems zs z t' t1 t2 =
@@ -499,7 +499,7 @@
             handle SAME () => do_term (t :: seen) ts
         in
           case t of
-            Const (@{const_name "op ="}, _) $ t1 $ t2 => do_eq true t1 t2
+            Const (@{const_name HOL.eq}, _) $ t1 $ t2 => do_eq true t1 t2
           | _ => do_term (t :: seen) ts
         end
   in do_term end
@@ -653,7 +653,7 @@
 
 fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
   | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
-  | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
+  | params_in_equation (Const (@{const_name HOL.eq}, _) $ t1 $ _) =
     snd (strip_comb t1)
   | params_in_equation _ = []
 
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -179,7 +179,7 @@
 
 fun translate_literal ctxt constant_table t =
   case strip_comb t of
-    (Const (@{const_name "op ="}, _), [l, r]) =>
+    (Const (@{const_name HOL.eq}, _), [l, r]) =>
       let
         val l' = translate_term ctxt constant_table l
         val r' = translate_term ctxt constant_table r
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -411,7 +411,7 @@
 fun conjuncts t = conjuncts_aux t [];
 
 fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
-  | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true
+  | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
   | is_equationlike_term _ = false
   
 val is_equationlike = is_equationlike_term o prop_of 
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -587,7 +587,7 @@
 
 fun preprocess_elim ctxt elimrule =
   let
-    fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
+    fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, T) $ lhs $ rhs)) =
        HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
      | replace_eqs t = t
     val thy = ProofContext.theory_of ctxt
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -111,7 +111,7 @@
 
 fun mk_meta_equation th =
   case prop_of th of
-    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
+    Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => th RS @{thm eq_reflection}
   | _ => th
 
 val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
@@ -217,7 +217,7 @@
    @{const_name "==>"},
    @{const_name Trueprop},
    @{const_name Not},
-   @{const_name "op ="},
+   @{const_name HOL.eq},
    @{const_name HOL.implies},
    @{const_name All},
    @{const_name Ex}, 
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -122,8 +122,8 @@
 ( case (term_of ct) of
   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$_) =>
+| Const (@{const_name HOL.eq},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
+| Const (@{const_name Not},_) $ (Const (@{const_name HOL.eq},_)$y$_) =>
   if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
 | Const (@{const_name Orderings.less}, _) $ y$ z =>
    if term_of x aconv y then Lt (Thm.dest_arg ct)
@@ -274,7 +274,7 @@
   | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
   | lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) =
     HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
-  | lin (vs as x::_) ((b as Const(@{const_name "op ="},_))$s$t) =
+  | lin (vs as x::_) ((b as Const(@{const_name HOL.eq},_))$s$t) =
      (case lint vs (subC$t$s) of
       (t as a$(m$c$y)$r) =>
         if x <> y then b$zero$t
@@ -345,7 +345,7 @@
    case (term_of t) of
     Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
     if x aconv y andalso member (op =)
-      ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
+      [@{const_name HOL.eq}, @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
     then (ins (dest_number c) acc,dacc) else (acc,dacc)
   | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
     if x aconv y andalso member (op =)
@@ -387,7 +387,7 @@
   | 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 =)
-      ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
+      [@{const_name HOL.eq}, @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
     then cv (l div dest_number c) t else Thm.reflexive t
   | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
     if x=y andalso member (op =)
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Qelim/qelim.ML
--- a/src/HOL/Tools/Qelim/qelim.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -26,7 +26,7 @@
     Const(s,T)$_$_ => 
        if domain_type T = HOLogic.boolT
           andalso member (op =) [@{const_name HOL.conj}, @{const_name HOL.disj},
-            @{const_name HOL.implies}, @{const_name "op ="}] s
+            @{const_name HOL.implies}, @{const_name HOL.eq}] s
        then binop_conv (conv env) p 
        else atcv env p
   | Const(@{const_name Not},_)$_ => arg_conv (conv env) p
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -338,7 +338,7 @@
       => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
 
     (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
-| (Const (@{const_name "op ="},_) $
+| (Const (@{const_name HOL.eq},_) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
       => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
@@ -350,7 +350,7 @@
       => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
 
     (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
-| Const (@{const_name "op ="},_) $
+| Const (@{const_name HOL.eq},_) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
       => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
@@ -370,13 +370,13 @@
     (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
       => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
 
-| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
+| Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
    (rtac @{thm refl} ORELSE'
     (equals_rsp_tac R ctxt THEN' RANGE [
        quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
 
     (* reflexivity of operators arising from Cong_tac *)
-| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
+| Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
 
    (* respectfulness of constants; in particular of a simple relation *)
 | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -267,7 +267,7 @@
   map_types (Envir.subst_type ty_inst) trm
 end
 
-fun is_eq (Const (@{const_name "op ="}, _)) = true
+fun is_eq (Const (@{const_name HOL.eq}, _)) = true
   | is_eq _ = false
 
 fun mk_rel_compose (trm1, trm2) =
@@ -539,12 +539,12 @@
        end
 
   | (* equalities need to be replaced by appropriate equivalence relations *)
-    (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
+    (Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) =>
          if ty = ty' then rtrm
          else equiv_relation ctxt (domain_type ty, domain_type ty')
 
   | (* in this case we just check whether the given equivalence relation is correct *)
-    (rel, Const (@{const_name "op ="}, ty')) =>
+    (rel, Const (@{const_name HOL.eq}, ty')) =>
        let
          val rel_ty = fastype_of rel
          val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
@@ -680,7 +680,7 @@
         if T = T' then rtrm
         else mk_repabs ctxt (T, T') rtrm
 
-  | (_, Const (@{const_name "op ="}, _)) => rtrm
+  | (_, Const (@{const_name HOL.eq}, _)) => rtrm
 
   | (_, Const (_, T')) =>
       let
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/SMT/smt_monomorph.ML
--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -16,7 +16,7 @@
 
 val ignored = member (op =) [
   @{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If},
-  @{const_name "op ="}, @{const_name zero_class.zero},
+  @{const_name HOL.eq}, @{const_name zero_class.zero},
   @{const_name one_class.one}, @{const_name number_of}]
 
 fun is_const f (n, T) = not (ignored n) andalso f T
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -252,7 +252,7 @@
 
 fun norm_def ctxt thm =
   (case Thm.prop_of thm of
-    @{term Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ Abs _) =>
+    @{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
       norm_def ctxt (thm RS @{thm fun_cong})
   | Const (@{const_name "=="}, _) $ _ $ Abs _ =>
       norm_def ctxt (thm RS @{thm meta_eq_to_obj_eq})
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -162,12 +162,12 @@
   | 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 HOL.eq} = SOME "iff"
   | conn @{const_name If} = SOME "if_then_else"
   | conn _ = NONE
 
 fun pred @{const_name distinct} _ = SOME "distinct"
-  | pred @{const_name "op ="} _ = SOME "="
+  | pred @{const_name HOL.eq} _ = SOME "="
   | pred @{const_name term_eq} _ = SOME "="
   | pred @{const_name less} T = if_int_type T "<"
   | pred @{const_name less_eq} T = if_int_type T "<="
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -176,7 +176,7 @@
 fun mk_nary _ cu [] = cu
   | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
 
-val eq = mk_inst_pair destT1 @{cpat "op ="}
+val eq = mk_inst_pair destT1 @{cpat HOL.eq}
 fun mk_eq ct cu = Thm.mk_binop (instT' ct eq) ct cu
 
 val if_term = mk_inst_pair (destT1 o destT2) @{cpat If}
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/SMT/z3_proof_literals.ML
--- a/src/HOL/Tools/SMT/z3_proof_literals.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_literals.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -234,7 +234,7 @@
         @{term Not} $ (@{term Not} $ t) => (T.compose dnegI, lookup t)
       | @{term Not} $ (@{term "op = :: bool => _"} $ t $ (@{term Not} $ u)) =>
           (T.compose negIffI, lookup (iff_const $ u $ t))
-      | @{term Not} $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u) =>
+      | @{term Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
           let fun rewr lit = lit COMP @{thm not_sym}
           in (rewr, lookup (@{term Not} $ (eq $ u $ t))) end
       | _ =>
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -199,7 +199,7 @@
       | @{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 HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
       | Const (@{const_name distinct}, _) $ _ =>
           if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
           else fresh_abstraction cvs ct
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -83,7 +83,7 @@
    (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
 fun extensionalize_theorem th =
   case prop_of th of
-    _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
+    _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _]))
          $ _ $ Abs (s, _, _)) => extensionalize_theorem (th RS fun_cong_all)
   | _ => th
 
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Sledgehammer/metis_clauses.ML
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -94,7 +94,7 @@
 val const_trans_table =
   Symtab.make [(@{type_name Product_Type.prod}, "prod"),
                (@{type_name Sum_Type.sum}, "sum"),
-               (@{const_name "op ="}, "equal"),
+               (@{const_name HOL.eq}, "equal"),
                (@{const_name HOL.conj}, "and"),
                (@{const_name HOL.disj}, "or"),
                (@{const_name HOL.implies}, "implies"),
@@ -111,7 +111,7 @@
 
 (* Invert the table of translations between Isabelle and ATPs. *)
 val const_trans_table_inv =
-  Symtab.update ("fequal", @{const_name "op ="})
+  Symtab.update ("fequal", @{const_name HOL.eq})
                 (Symtab.make (map swap (Symtab.dest const_trans_table)))
 
 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
@@ -185,8 +185,8 @@
     SOME c' => c'
   | NONE => ascii_of c
 
-(* "op =" MUST BE "equal" because it's built into ATPs. *)
-fun make_fixed_const @{const_name "op ="} = "equal"
+(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
+fun make_fixed_const @{const_name HOL.eq} = "equal"
   | make_fixed_const c = const_prefix ^ lookup_const c
 
 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -224,7 +224,7 @@
 
 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
 
-fun smart_invert_const "fequal" = @{const_name "op ="}
+fun smart_invert_const "fequal" = @{const_name HOL.eq}
   | smart_invert_const s = invert_const s
 
 fun hol_type_from_metis_term _ (Metis.Term.Var v) =
@@ -264,7 +264,7 @@
             end
         | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
       and applic_to_tt ("=",ts) =
-            Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
+            Term (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
         | applic_to_tt (a,ts) =
             case strip_prefix_and_unascii const_prefix a of
                 SOME b =>
@@ -311,7 +311,7 @@
                   SOME w =>  mk_var(w, dummyT)
                 | NONE   => mk_var(v, dummyT))
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
-            Const (@{const_name "op ="}, HOLogic.typeT)
+            Const (@{const_name HOL.eq}, HOLogic.typeT)
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
            (case strip_prefix_and_unascii const_prefix x of
                 SOME c => Const (smart_invert_const c, dummyT)
@@ -325,7 +325,7 @@
             cvt tm1 $ cvt tm2
         | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
         | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
-            list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
+            list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
         | cvt (t as Metis.Term.Fn (x, [])) =
            (case strip_prefix_and_unascii const_prefix x of
                 SOME c => Const (smart_invert_const c, dummyT)
@@ -480,7 +480,7 @@
       val c_t = cterm_incr_types thy refl_idx i_t
   in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
 
-fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0  (*equality has no type arguments*)
+fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0  (*equality has no type arguments*)
   | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
   | get_ty_arg_size _ _ = 0;
 
@@ -529,13 +529,13 @@
                       " isa-term: " ^  Syntax.string_of_term ctxt tm ^
                       " fol-term: " ^ Metis.Term.toString t)
       fun path_finder FO tm ps _ = path_finder_FO tm ps
-        | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
+        | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
              (*equality: not curried, as other predicates are*)
              if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
              else path_finder_HO tm (p::ps)        (*1 selects second operand*)
         | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
              path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
-        | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
+        | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
                             (Metis.Term.Fn ("=", [t1,t2])) =
              (*equality: not curried, as other predicates are*)
              if p=0 then path_finder_FT tm (0::1::ps)
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -121,7 +121,7 @@
    handled specially via "fequal". *)
 val boring_consts =
   [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
-   @{const_name "op ="}]
+   @{const_name HOL.eq}]
 
 (* Add a pconstant to the table, but a [] entry means a standard
    connective, which we ignore.*)
@@ -177,7 +177,7 @@
       | @{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 =>
+      | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
         fold (do_term_or_formula T) [t1, t2]
       | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
         $ t1 $ t2 $ t3 =>
@@ -557,7 +557,7 @@
       | (_, @{const Not} $ t1) => do_formula (not pos) t1
       | (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 HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
       | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
       | _ => false
   in do_formula true end
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -315,7 +315,7 @@
           | _ => raise FO_TERM us
         else case strip_prefix_and_unascii const_prefix a of
           SOME "equal" =>
-          list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
+          list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT),
                      map (aux NONE []) us)
         | SOME b =>
           let
@@ -527,7 +527,7 @@
   | is_bad_free _ _ = false
 
 (* Vampire is keen on producing these. *)
-fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _)
+fun is_trivial_formula (@{const Not} $ (Const (@{const_name HOL.eq}, _)
                                         $ t1 $ t2)) = (t1 aconv t2)
   | is_trivial_formula _ = false
 
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -73,7 +73,7 @@
       | @{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 =>
+      | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
         do_conn bs AIff t1 t2
       | _ => (fn ts => do_term bs (Envir.eta_contract t)
                        |>> AAtom ||> union (op =) ts)
@@ -97,7 +97,7 @@
       | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
                                         Type (_, [_, res_T])]))
                     $ t2 $ Abs (var_s, var_T, t')) =
-        if s = @{const_name "op ="} orelse s = @{const_name "=="} then
+        if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
           let val var_t = Var ((var_s, j), var_T) in
             Const (s, T' --> T' --> res_T)
               $ betapply (t2, var_t) $ subst_bound (var_t, t')
@@ -128,7 +128,7 @@
           | (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}, _])))
+          | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
               $ t1 $ t2 =>
             t0 $ aux Ts t1 $ aux Ts t2
           | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/TFL/dcterm.ML
--- a/src/HOL/Tools/TFL/dcterm.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/TFL/dcterm.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -127,7 +127,7 @@
 
 val dest_neg    = dest_monop @{const_name Not}
 val dest_pair   = dest_binop @{const_name Pair}
-val dest_eq     = dest_binop @{const_name "op ="}
+val dest_eq     = dest_binop @{const_name HOL.eq}
 val dest_imp    = dest_binop @{const_name HOL.implies}
 val dest_conj   = dest_binop @{const_name HOL.conj}
 val dest_disj   = dest_binop @{const_name HOL.disj}
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/TFL/post.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -67,7 +67,7 @@
 val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
 fun mk_meta_eq r = case concl_of r of
      Const("==",_)$_$_ => r
-  |   _ $(Const(@{const_name "op ="},_)$_$_) => r RS eq_reflection
+  |   _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection
   |   _ => r RS P_imp_P_eq_True
 
 (*Is this the best way to invoke the simplifier??*)
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/TFL/usyntax.ML
--- a/src/HOL/Tools/TFL/usyntax.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -244,7 +244,7 @@
      end
   | dest_abs _ _ =  raise USYN_ERR "dest_abs" "not an abstraction";
 
-fun dest_eq(Const(@{const_name "op ="},_) $ M $ N) = {lhs=M, rhs=N}
+fun dest_eq(Const(@{const_name HOL.eq},_) $ M $ N) = {lhs=M, rhs=N}
   | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
 
 fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N}
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -98,7 +98,7 @@
   | 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 HOL.eq}, Type ("fun", @{typ bool} :: _)) $ _ $ _)       = false
   | is_atom (Const (@{const_name Not}, _) $ _)                                         = false
   | is_atom _                                                              = true;
 
@@ -205,7 +205,7 @@
 	in
 		make_nnf_imp OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
+  | make_nnf_thm thy (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
 	let
 		val thm1 = make_nnf_thm thy x
 		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
@@ -239,7 +239,7 @@
 	in
 		make_nnf_not_imp OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
+  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
 	let
 		val thm1 = make_nnf_thm thy x
 		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/groebner.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -409,7 +409,7 @@
     | _  => false;
 fun is_eq t =
  case term_of t of
- (Const(@{const_name "op ="},_)$_$_) => true
+ (Const(@{const_name HOL.eq},_)$_$_) => true
 | _  => false;
 
 fun end_itlist f l =
@@ -923,7 +923,7 @@
 
 fun find_term bounds tm =
   (case term_of tm of
-    Const (@{const_name "op ="}, T) $ _ $ _ =>
+    Const (@{const_name HOL.eq}, T) $ _ $ _ =>
       if domain_type T = HOLogic.boolT then find_args bounds tm
       else dest_arg tm
   | Const (@{const_name Not}, _) $ _ => find_term bounds (dest_arg tm)
@@ -985,7 +985,7 @@
 
 local
  fun lhs t = case term_of t of
-  Const(@{const_name "op ="},_)$_$_ => Thm.dest_arg1 t
+  Const(@{const_name HOL.eq},_)$_$_ => Thm.dest_arg1 t
  | _=> raise CTERM ("ideal_tac - lhs",[t])
  fun exitac NONE = no_tac
    | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/hologic.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -236,10 +236,10 @@
 fun dest_not (Const ("HOL.Not", _) $ t) = t
   | dest_not t = raise TERM ("dest_not", [t]);
 
-fun eq_const T = Const ("op =", T --> T --> boolT);
+fun eq_const T = Const ("HOL.eq", T --> T --> boolT);
 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
 
-fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
+fun dest_eq (Const ("HOL.eq", _) $ lhs $ rhs) = (lhs, rhs)
   | dest_eq t = raise TERM ("dest_eq", [t])
 
 fun all_const T = Const ("HOL.All", [T --> boolT] ---> boolT);
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -182,7 +182,7 @@
   in
     case concl_of thm of
       Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
-    | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => eq2mono thm
+    | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq2mono thm
     | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
       dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
         (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -52,7 +52,7 @@
     fun thyname_of s = (case optmod of
       NONE => Codegen.thyname_of_const thy s | SOME s => s);
   in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of
-      SOME (Const (@{const_name "op ="}, _), [t, _]) =>
+      SOME (Const (@{const_name HOL.eq}, _), [t, _]) =>
         (case head_of t of
           Const (s, _) =>
             CodegenData.put {intros = intros, graph = graph,
@@ -188,7 +188,7 @@
         end)) (AList.lookup op = modes name)
 
   in (case strip_comb t of
-      (Const (@{const_name "op ="}, Type (_, [T, _])), _) =>
+      (Const (@{const_name HOL.eq}, Type (_, [T, _])), _) =>
         [Mode ((([], [1]), false), [1], []), Mode ((([], [2]), false), [2], [])] @
         (if is_eqT T then [Mode ((([], [1, 2]), false), [1, 2], [])] else [])
     | (Const (name, _), args) => the_default default (mk_modes name args)
@@ -344,7 +344,7 @@
   end;
 
 fun modename module s (iss, is) gr =
-  let val (id, gr') = if s = @{const_name "op ="} then (("", "equal"), gr)
+  let val (id, gr') = if s = @{const_name HOL.eq} then (("", "equal"), gr)
     else mk_const_id module s gr
   in (space_implode "__"
     (mk_qual_id module id ::
@@ -363,7 +363,7 @@
   | compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr =
       (case strip_comb t of
          (Const (name, _), args) =>
-           if name = @{const_name "op ="} orelse AList.defined op = modes name then
+           if name = @{const_name HOL.eq} orelse AList.defined op = modes name then
              let
                val (args1, args2) = chop (length ms) args;
                val ((ps, mode_id), gr') = gr |> fold_map
@@ -581,7 +581,7 @@
 
       fun dest_prem (_ $ (Const (@{const_name Set.member}, _) $ t $ u)) =
             Prem ([t], Envir.beta_eta_contract u, true)
-        | dest_prem (_ $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u)) =
+        | dest_prem (_ $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u)) =
             Prem ([t, u], eq, false)
         | dest_prem (_ $ t) =
             (case strip_comb t of
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -265,7 +265,7 @@
 
 fun add ctxt thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
   case prop_of thm of
-    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, Type (_, [T, _])) $ lhs $ rhs) =>
+    Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ lhs $ rhs) =>
       (case body_type T of
          @{typ bool} =>
            let
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/int_arith.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -51,7 +51,7 @@
 
 fun check (Const (@{const_name Groups.one}, @{typ int})) = false
   | check (Const (@{const_name Groups.one}, _)) = true
-  | check (Const (s, _)) = member (op =) [@{const_name "op ="},
+  | check (Const (s, _)) = member (op =) [@{const_name HOL.eq},
       @{const_name Groups.times}, @{const_name Groups.uminus},
       @{const_name Groups.minus}, @{const_name Groups.plus},
       @{const_name Groups.zero},
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -229,7 +229,7 @@
   case rel of
     @{const_name Orderings.less}    => SOME (p, i, "<", q, j)
   | @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j)
-  | "op ="              => SOME (p, i, "=", q, j)
+  | @{const_name HOL.eq}            => SOME (p, i, "=", q, j)
   | _                   => NONE
 end handle Rat.DIVZERO => NONE;
 
@@ -427,7 +427,7 @@
         val t2'             = incr_boundvars 1 t2
         val t1_lt_t2        = Const (@{const_name Orderings.less},
                                 split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
-        val t1_eq_t2_plus_d = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
+        val t1_eq_t2_plus_d = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
                                 (Const (@{const_name Groups.plus},
                                   split_type --> split_type --> split_type) $ t2' $ d)
         val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -447,7 +447,7 @@
                             (map (incr_boundvars 1) rev_terms)
         val terms2      = map (subst_term [(split_term, zero_nat)]) rev_terms
         val t1'         = incr_boundvars 1 t1
-        val t1_eq_nat_n = Const (@{const_name "op ="}, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
+        val t1_eq_nat_n = Const (@{const_name HOL.eq}, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
                             (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
         val t1_lt_zero  = Const (@{const_name Orderings.less},
                             HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
@@ -471,13 +471,13 @@
                                         (map (incr_boundvars 2) rev_terms)
         val t1'                     = incr_boundvars 2 t1
         val t2'                     = incr_boundvars 2 t2
-        val t2_eq_zero              = Const (@{const_name "op ="},
+        val t2_eq_zero              = Const (@{const_name HOL.eq},
                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
-        val t2_neq_zero             = HOLogic.mk_not (Const (@{const_name "op ="},
+        val t2_neq_zero             = HOLogic.mk_not (Const (@{const_name HOL.eq},
                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
         val j_lt_t2                 = Const (@{const_name Orderings.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
-        val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
+        val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
                                        (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
                                          (Const (@{const_name Groups.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -503,13 +503,13 @@
                                         (map (incr_boundvars 2) rev_terms)
         val t1'                     = incr_boundvars 2 t1
         val t2'                     = incr_boundvars 2 t2
-        val t2_eq_zero              = Const (@{const_name "op ="},
+        val t2_eq_zero              = Const (@{const_name HOL.eq},
                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
-        val t2_neq_zero             = HOLogic.mk_not (Const (@{const_name "op ="},
+        val t2_neq_zero             = HOLogic.mk_not (Const (@{const_name HOL.eq},
                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
         val j_lt_t2                 = Const (@{const_name Orderings.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
-        val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
+        val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
                                        (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
                                          (Const (@{const_name Groups.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -541,7 +541,7 @@
                                         (map (incr_boundvars 2) rev_terms)
         val t1'                     = incr_boundvars 2 t1
         val t2'                     = incr_boundvars 2 t2
-        val t2_eq_zero              = Const (@{const_name "op ="},
+        val t2_eq_zero              = Const (@{const_name HOL.eq},
                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
         val zero_lt_t2              = Const (@{const_name Orderings.less},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
@@ -555,7 +555,7 @@
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t2_lt_j                 = Const (@{const_name Orderings.less},
                                         split_type --> split_type--> HOLogic.boolT) $ t2' $ j
-        val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
+        val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
                                        (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
                                          (Const (@{const_name Groups.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -595,7 +595,7 @@
                                         (map (incr_boundvars 2) rev_terms)
         val t1'                     = incr_boundvars 2 t1
         val t2'                     = incr_boundvars 2 t2
-        val t2_eq_zero              = Const (@{const_name "op ="},
+        val t2_eq_zero              = Const (@{const_name HOL.eq},
                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
         val zero_lt_t2              = Const (@{const_name Orderings.less},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
@@ -609,7 +609,7 @@
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t2_lt_j                 = Const (@{const_name Orderings.less},
                                         split_type --> split_type--> HOLogic.boolT) $ t2' $ j
-        val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
+        val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
                                        (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
                                          (Const (@{const_name Groups.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -183,7 +183,7 @@
 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
 
 (*Literals like X=X are tautologous*)
-fun taut_poslit (Const(@{const_name "op ="},_) $ t $ u) = t aconv u
+fun taut_poslit (Const(@{const_name HOL.eq},_) $ t $ u) = t aconv u
   | taut_poslit (Const(@{const_name True},_)) = true
   | taut_poslit _ = false;
 
@@ -213,7 +213,7 @@
        case HOLogic.dest_Trueprop (concl_of th) of
           (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 HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
+        | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ 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*)
@@ -222,7 +222,7 @@
 
 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 (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _)) = 1
   | notequal_lits_count _ = 0;
 
 (*Simplify a clause by applying reflexivity to its negated equality literals*)
@@ -280,7 +280,7 @@
     | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
         if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
              else sum (signed_nclauses (not b) t) (signed_nclauses b u)
-    | signed_nclauses b (Const(@{const_name "op ="}, Type ("fun", [T, _])) $ t $ u) =
+    | signed_nclauses b (Const(@{const_name HOL.eq}, Type ("fun", [T, _])) $ t $ u) =
         if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
             if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
                           (prod (signed_nclauses (not b) u) (signed_nclauses b t))
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/nat_arith.ML
--- a/src/HOL/Tools/nat_arith.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/nat_arith.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -62,7 +62,7 @@
 (struct
   open CommonCancelSums;
   val mk_bal = HOLogic.mk_eq;
-  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT;
   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
 end);
 
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -168,7 +168,7 @@
  (open CancelNumeralsCommon
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
-  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
   val bal_add1 = @{thm nat_eq_add_iff1} RS trans
   val bal_add2 = @{thm nat_eq_add_iff2} RS trans
 );
@@ -300,7 +300,7 @@
  (open CancelNumeralFactorCommon
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
-  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
   val cancel = @{thm nat_mult_eq_cancel1} RS trans
   val neg_exchanges = false
 )
@@ -380,7 +380,7 @@
  (open CancelFactorCommon
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
-  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
   fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj}
 );
 
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -222,7 +222,7 @@
  (open CancelNumeralsCommon
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
-  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
   val bal_add1 = @{thm eq_add_iff1} RS trans
   val bal_add2 = @{thm eq_add_iff2} RS trans
 );
@@ -401,7 +401,7 @@
  (open CancelNumeralFactorCommon
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
-  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
   val cancel = @{thm mult_cancel_left} RS trans
   val neg_exchanges = false
 )
@@ -516,7 +516,7 @@
  (open CancelFactorCommon
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
-  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
   fun simp_conv _ _ = SOME @{thm mult_cancel_left}
 );
 
@@ -606,7 +606,7 @@
 local
  val zr = @{cpat "0"}
  val zT = ctyp_of_term zr
- val geq = @{cpat "op ="}
+ val geq = @{cpat HOL.eq}
  val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
  val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
  val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
@@ -676,7 +676,7 @@
         val T = ctyp_of_term c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name "op ="},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
+  | Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
       let
         val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
         val _ = map is_number [a,b,c]
@@ -697,7 +697,7 @@
         val T = ctyp_of_term c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name "op ="},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
+  | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
     let
       val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
         val _ = map is_number [a,b,c]
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -40,7 +40,7 @@
       end
   | avoid_value thy thms = thms;
 
-fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
+fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name HOL.eq} then ([], "") else
   let
     val c = AxClass.unoverload_const thy (raw_c, T);
     val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/record.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -1342,7 +1342,7 @@
 val eq_simproc =
   Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
     (fn thy => fn _ => fn t =>
-      (case t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ =>
+      (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
         (case rec_id ~1 T of
           "" => NONE
         | name =>
@@ -1405,12 +1405,12 @@
                 else raise TERM ("", [x]);
               val sel' = Const (sel, Tsel) $ Bound 0;
               val (l, r) = if lr then (sel', x') else (x', sel');
-            in Const (@{const_name "op ="}, Teq) $ l $ r end
+            in Const (@{const_name HOL.eq}, Teq) $ l $ r end
           else raise TERM ("", [Const (sel, Tsel)]);
 
-        fun dest_sel_eq (Const (@{const_name "op ="}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
+        fun dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
               (true, Teq, (sel, Tsel), X)
-          | dest_sel_eq (Const (@{const_name "op ="}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
+          | dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
               (false, Teq, (sel, Tsel), X)
           | dest_sel_eq _ = raise TERM ("", []);
       in
@@ -1845,7 +1845,7 @@
     val eq =
       (HOLogic.mk_Trueprop o HOLogic.mk_eq)
         (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
-         Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
+         Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT));
     fun tac eq_def =
       Class.intro_classes_tac []
       THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def])
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -647,7 +647,7 @@
       | Const (@{const_name Hilbert_Choice.Eps}, _) => t
       | Const (@{const_name All}, _) => t
       | Const (@{const_name Ex}, _) => t
-      | Const (@{const_name "op ="}, _) => t
+      | Const (@{const_name HOL.eq}, _) => t
       | Const (@{const_name HOL.conj}, _) => t
       | Const (@{const_name HOL.disj}, _) => t
       | Const (@{const_name HOL.implies}, _) => t
@@ -823,7 +823,7 @@
         end
       | 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 HOL.eq}, T) => collect_type_axioms T axs
       | Const (@{const_name HOL.conj}, _) => axs
       | Const (@{const_name HOL.disj}, _) => axs
       | Const (@{const_name HOL.implies}, _) => axs
@@ -1850,16 +1850,16 @@
       end
     | Const (@{const_name Ex}, _) =>
       SOME (interpret thy model args (eta_expand t 1))
-    | Const (@{const_name "op ="}, _) $ t1 $ t2 =>  (* similar to "==" (Pure) *)
+    | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>  (* similar to "==" (Pure) *)
       let
         val (i1, m1, a1) = interpret thy model args t1
         val (i2, m2, a2) = interpret thy m1 a1 t2
       in
         SOME (make_equality (i1, i2), m2, a2)
       end
-    | Const (@{const_name "op ="}, _) $ t1 =>
+    | Const (@{const_name HOL.eq}, _) $ t1 =>
       SOME (interpret thy model args (eta_expand t 1))
-    | Const (@{const_name "op ="}, _) =>
+    | Const (@{const_name HOL.eq}, _) =>
       SOME (interpret thy model args (eta_expand t 2))
     | Const (@{const_name HOL.conj}, _) $ t1 $ t2 =>
       (* 3-valued logic *)
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -10,7 +10,7 @@
 structure Quantifier1 = Quantifier1Fun
 (struct
   (*abstract syntax*)
-  fun dest_eq ((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME (c, s, t)
+  fun dest_eq ((c as Const(@{const_name HOL.eq},_)) $ s $ t) = SOME (c, s, t)
     | dest_eq _ = NONE;
   fun dest_conj ((c as Const(@{const_name HOL.conj},_)) $ s $ t) = SOME (c, s, t)
     | dest_conj _ = NONE;
@@ -44,7 +44,7 @@
 fun mk_eq th = case concl_of th
   (*expects Trueprop if not == *)
   of Const (@{const_name "=="},_) $ _ $ _ => th
-   | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => mk_meta_eq th
+   | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th
    | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
    | _ => th RS @{thm Eq_TrueI}
 
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/ex/Meson_Test.thy
--- a/src/HOL/ex/Meson_Test.thy	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Mon Aug 30 09:35:30 2010 +0200
@@ -10,7 +10,7 @@
   below and constants declared in HOL!
 *}
 
-hide_const (open) implies union inter subset sum quotient 
+hide_const (open) eq implies union inter subset sum quotient 
 
 text {*
   Test data for the MESON proof procedure
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/ex/SVC_Oracle.thy
--- a/src/HOL/ex/SVC_Oracle.thy	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy	Mon Aug 30 09:35:30 2010 +0200
@@ -94,7 +94,7 @@
       | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
       | fm ((c as Const(@{const_name True}, _))) = c
       | fm ((c as Const(@{const_name False}, _))) = c
-      | fm (t as Const(@{const_name "op ="},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+      | fm (t as Const(@{const_name HOL.eq},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
       | fm (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
       | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
       | fm t = replace t
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -95,7 +95,7 @@
            | Const(@{const_name Not}, _)    => apply c (map tag ts)
            | Const(@{const_name True}, _)   => (c, false)
            | Const(@{const_name False}, _)  => (c, false)
-           | Const(@{const_name "op ="}, Type ("fun", [T,_])) =>
+           | Const(@{const_name HOL.eq}, Type ("fun", [T,_])) =>
                  if T = HOLogic.boolT then
                      (*biconditional: with int/nat comparisons below?*)
                      let val [t1,t2] = ts
@@ -200,7 +200,7 @@
             Buildin("AND",   (*unfolding uses both polarities*)
                          [Buildin("=>", [fm (not pos) p, fm pos q]),
                           Buildin("=>", [fm (not pos) q, fm pos p])])
-      | fm pos (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ x $ y) =
+      | fm pos (t as Const(@{const_name HOL.eq}, Type ("fun", [T,_])) $ x $ y) =
             let val tx = tm x and ty = tm y
                 in if pos orelse T = HOLogic.realT then
                        Buildin("=", [tx, ty])
diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOLCF/Tools/Domain/domain_library.ML
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -190,9 +190,9 @@
 
 fun mk_All  (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
 
-infixr 0 ===>;  fun S ===> T = %%:"==>" $ S $ T;
-infix 0 ==;     fun S ==  T = %%:"==" $ S $ T;
-infix 1 ===;    fun S === T = %%:"op =" $ S $ T;
+infixr 0 ===>;  fun S ===> T = %%: "==>" $ S $ T;
+infix 0 ==;     fun S ==  T = %%: "==" $ S $ T;
+infix 1 ===;    fun S === T = %%: @{const_name HOL.eq} $ S $ T;
 infix 1 ~=;     fun S ~=  T = HOLogic.mk_not (S === T);
 
 infix 9 `  ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x;