formerly unnamed infix equality now named HOL.eq
authorhaftmann
Sat Aug 28 16:14:32 2010 +0200 (2010-08-28)
changeset 388644abe644fcea5
parent 38859 053c69cb4a0e
child 38865 43c934dd4bc3
formerly unnamed infix equality now named HOL.eq
NEWS
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/commutative_ring_tac.ML
src/HOL/Decision_Procs/ferrante_rackoff.ML
src/HOL/Decision_Procs/langford.ML
src/HOL/HOL.thy
src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
src/HOL/Import/HOLLight/hollight.imp
src/HOL/Import/hol4rews.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Library/OptionalSugar.thy
src/HOL/Library/reflection.ML
src/HOL/Mutabelle/Mutabelle.thy
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Set.thy
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/Nitpick/minipick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/qelim.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/SMT/smt_monomorph.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_interface.ML
src/HOL/Tools/SMT/z3_proof_literals.ML
src/HOL/Tools/SMT/z3_proof_tools.ML
src/HOL/Tools/Sledgehammer/clausifier.ML
src/HOL/Tools/Sledgehammer/metis_clauses.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
src/HOL/Tools/TFL/dcterm.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/TFL/usyntax.ML
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/nat_arith.ML
src/HOL/Tools/nat_numeral_simprocs.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/record.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/simpdata.ML
src/HOL/ex/Meson_Test.thy
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/svc_funcs.ML
src/HOLCF/Tools/Domain/domain_library.ML
     1.1 --- a/NEWS	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/NEWS	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -136,6 +136,7 @@
     1.4      op & ~> HOL.conj
     1.5      op | ~> HOL.disj
     1.6      op --> ~> HOL.implies
     1.7 +    op = ~> HOL.eq
     1.8      Not ~> HOL.Not
     1.9      The ~> HOL.The
    1.10      All ~> HOL.All
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sat Aug 28 20:24:40 2010 +0800
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Aug 28 16:14:32 2010 +0200
     2.3 @@ -3305,7 +3305,7 @@
     2.4                               (Const (@{const_name Set.member}, _) $
     2.5                                Free (name, _) $ _)) = name
     2.6          | variable_of_bound (Const (@{const_name Trueprop}, _) $
     2.7 -                             (Const (@{const_name "op ="}, _) $
     2.8 +                             (Const (@{const_name HOL.eq}, _) $
     2.9                                Free (name, _) $ _)) = name
    2.10          | variable_of_bound t = raise TERM ("variable_of_bound", [t])
    2.11  
     3.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sat Aug 28 20:24:40 2010 +0800
     3.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sat Aug 28 16:14:32 2010 +0200
     3.3 @@ -519,9 +519,9 @@
     3.4    val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
     3.5    fun h x t =
     3.6     case term_of t of
     3.7 -     Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
     3.8 +     Const(@{const_name HOL.eq}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
     3.9                              else Ferrante_Rackoff_Data.Nox
    3.10 -   | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
    3.11 +   | @{term "Not"}$(Const(@{const_name HOL.eq}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
    3.12                              else Ferrante_Rackoff_Data.Nox
    3.13     | b$y$z => if Term.could_unify (b, lt) then
    3.14                   if term_of x aconv y then Ferrante_Rackoff_Data.Lt
    3.15 @@ -771,7 +771,7 @@
    3.16        in rth end
    3.17      | _ => Thm.reflexive ct)
    3.18  
    3.19 -|  Const(@{const_name "op ="},_)$_$Const(@{const_name Groups.zero},_) =>
    3.20 +|  Const(@{const_name HOL.eq},_)$_$Const(@{const_name Groups.zero},_) =>
    3.21     (case whatis x (Thm.dest_arg1 ct) of
    3.22      ("c*x+t",[c,t]) =>
    3.23         let
    3.24 @@ -835,7 +835,7 @@
    3.25         val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    3.26     in rth end
    3.27  
    3.28 -| Const(@{const_name "op ="},_)$a$b =>
    3.29 +| Const(@{const_name HOL.eq},_)$a$b =>
    3.30     let val (ca,cb) = Thm.dest_binop ct
    3.31         val T = ctyp_of_term ca
    3.32         val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
    3.33 @@ -844,7 +844,7 @@
    3.34                (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
    3.35         val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    3.36     in rth end
    3.37 -| @{term "Not"} $(Const(@{const_name "op ="},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
    3.38 +| @{term "Not"} $(Const(@{const_name HOL.eq},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
    3.39  | _ => Thm.reflexive ct
    3.40  end;
    3.41  
    3.42 @@ -852,9 +852,9 @@
    3.43   let
    3.44    fun h x t =
    3.45     case term_of t of
    3.46 -     Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
    3.47 +     Const(@{const_name HOL.eq}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
    3.48                              else Ferrante_Rackoff_Data.Nox
    3.49 -   | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
    3.50 +   | @{term "Not"}$(Const(@{const_name HOL.eq}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
    3.51                              else Ferrante_Rackoff_Data.Nox
    3.52     | Const(@{const_name Orderings.less},_)$y$z =>
    3.53         if term_of x aconv y then Ferrante_Rackoff_Data.Lt
     4.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Aug 28 20:24:40 2010 +0800
     4.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Aug 28 16:14:32 2010 +0200
     4.3 @@ -912,7 +912,7 @@
     4.4  
     4.5  definition "lt p = (case p of CP (C c) \<Rightarrow> if 0>\<^sub>N c then T else F| _ \<Rightarrow> Lt p)"
     4.6  definition "le p = (case p of CP (C c) \<Rightarrow> if 0\<ge>\<^sub>N c then T else F | _ \<Rightarrow> Le p)"
     4.7 -definition "eq p = (case p of CP (C c) \<Rightarrow> if c = 0\<^sub>N then T else F | _ \<Rightarrow> Eq p)"
     4.8 +definition eq where "eq p = (case p of CP (C c) \<Rightarrow> if c = 0\<^sub>N then T else F | _ \<Rightarrow> Eq p)"
     4.9  definition "neq p = not (eq p)"
    4.10  
    4.11  lemma lt: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (lt p) = Ifm vs bs (Lt p)"
    4.12 @@ -2960,7 +2960,7 @@
    4.13  val ifft = @{term "op = :: bool => _"}
    4.14  fun llt rT = Const(@{const_name Orderings.less},rrT rT);
    4.15  fun lle rT = Const(@{const_name Orderings.less},rrT rT);
    4.16 -fun eqt rT = Const(@{const_name "op ="},rrT rT);
    4.17 +fun eqt rT = Const(@{const_name HOL.eq},rrT rT);
    4.18  fun rz rT = Const(@{const_name Groups.zero},rT);
    4.19  
    4.20  fun dest_nat t = case t of
    4.21 @@ -3021,7 +3021,7 @@
    4.22    | Const(@{const_name HOL.conj},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
    4.23    | Const(@{const_name HOL.disj},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
    4.24    | Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
    4.25 -  | Const(@{const_name "op ="},ty)$p$q => 
    4.26 +  | Const(@{const_name HOL.eq},ty)$p$q => 
    4.27         if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
    4.28         else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    4.29    | Const(@{const_name Orderings.less},_)$p$q => 
     5.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Sat Aug 28 20:24:40 2010 +0800
     5.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Sat Aug 28 16:14:32 2010 +0200
     5.3 @@ -65,7 +65,7 @@
     5.4  (* reification of the equation *)
     5.5  val cr_sort = @{sort "comm_ring_1"};
     5.6  
     5.7 -fun reif_eq thy (eq as Const(@{const_name "op ="}, Type("fun", [T, _])) $ lhs $ rhs) =
     5.8 +fun reif_eq thy (eq as Const(@{const_name HOL.eq}, Type("fun", [T, _])) $ lhs $ rhs) =
     5.9        if Sign.of_sort thy (T, cr_sort) then
    5.10          let
    5.11            val fs = OldTerm.term_frees eq;
     6.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sat Aug 28 20:24:40 2010 +0800
     6.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sat Aug 28 16:14:32 2010 +0200
     6.3 @@ -175,7 +175,7 @@
     6.4   let
     6.5    fun h bounds tm =
     6.6     (case term_of tm of
     6.7 -     Const (@{const_name "op ="}, T) $ _ $ _ =>
     6.8 +     Const (@{const_name HOL.eq}, T) $ _ $ _ =>
     6.9         if domain_type T = HOLogic.boolT then find_args bounds tm
    6.10         else Thm.dest_fun2 tm
    6.11     | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
     7.1 --- a/src/HOL/Decision_Procs/langford.ML	Sat Aug 28 20:24:40 2010 +0800
     7.2 +++ b/src/HOL/Decision_Procs/langford.ML	Sat Aug 28 16:14:32 2010 +0200
     7.3 @@ -116,7 +116,7 @@
     7.4  fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
     7.5  
     7.6  fun is_eqx x eq = case term_of eq of
     7.7 -   Const(@{const_name "op ="},_)$l$r => l aconv term_of x orelse r aconv term_of x
     7.8 +   Const(@{const_name HOL.eq},_)$l$r => l aconv term_of x orelse r aconv term_of x
     7.9   | _ => false ;
    7.10  
    7.11  local 
    7.12 @@ -176,7 +176,7 @@
    7.13   let
    7.14    fun h bounds tm =
    7.15     (case term_of tm of
    7.16 -     Const (@{const_name "op ="}, T) $ _ $ _ =>
    7.17 +     Const (@{const_name HOL.eq}, T) $ _ $ _ =>
    7.18         if domain_type T = HOLogic.boolT then find_args bounds tm
    7.19         else Thm.dest_fun2 tm
    7.20     | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
     8.1 --- a/src/HOL/HOL.thy	Sat Aug 28 20:24:40 2010 +0800
     8.2 +++ b/src/HOL/HOL.thy	Sat Aug 28 16:14:32 2010 +0200
     8.3 @@ -61,14 +61,8 @@
     8.4    disj          :: "[bool, bool] => bool"           (infixr "|" 30)
     8.5    implies       :: "[bool, bool] => bool"           (infixr "-->" 25)
     8.6  
     8.7 -setup Sign.root_path
     8.8 +  eq            :: "['a, 'a] => bool"               (infixl "=" 50)
     8.9  
    8.10 -consts
    8.11 -  "op ="        :: "['a, 'a] => bool"               (infixl "=" 50)
    8.12 -
    8.13 -setup Sign.local_path
    8.14 -
    8.15 -consts
    8.16    The           :: "('a => bool) => 'a"
    8.17    All           :: "('a => bool) => bool"           (binder "ALL " 10)
    8.18    Ex            :: "('a => bool) => bool"           (binder "EX " 10)
    8.19 @@ -78,7 +72,7 @@
    8.20  subsubsection {* Additional concrete syntax *}
    8.21  
    8.22  notation (output)
    8.23 -  "op ="  (infix "=" 50)
    8.24 +  eq  (infix "=" 50)
    8.25  
    8.26  abbreviation
    8.27    not_equal :: "['a, 'a] => bool"  (infixl "~=" 50) where
    8.28 @@ -89,15 +83,15 @@
    8.29  
    8.30  notation (xsymbols)
    8.31    Not  ("\<not> _" [40] 40) and
    8.32 -  HOL.conj  (infixr "\<and>" 35) and
    8.33 -  HOL.disj  (infixr "\<or>" 30) and
    8.34 -  HOL.implies  (infixr "\<longrightarrow>" 25) and
    8.35 +  conj  (infixr "\<and>" 35) and
    8.36 +  disj  (infixr "\<or>" 30) and
    8.37 +  implies  (infixr "\<longrightarrow>" 25) and
    8.38    not_equal  (infix "\<noteq>" 50)
    8.39  
    8.40  notation (HTML output)
    8.41    Not  ("\<not> _" [40] 40) and
    8.42 -  HOL.conj  (infixr "\<and>" 35) and
    8.43 -  HOL.disj  (infixr "\<or>" 30) and
    8.44 +  conj  (infixr "\<and>" 35) and
    8.45 +  disj  (infixr "\<or>" 30) and
    8.46    not_equal  (infix "\<noteq>" 50)
    8.47  
    8.48  abbreviation (iff)
    8.49 @@ -183,8 +177,8 @@
    8.50    True_or_False:  "(P=True) | (P=False)"
    8.51  
    8.52  finalconsts
    8.53 -  "op ="
    8.54 -  HOL.implies
    8.55 +  eq
    8.56 +  implies
    8.57    The
    8.58  
    8.59  definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where
    8.60 @@ -864,7 +858,7 @@
    8.61  
    8.62  setup {*
    8.63  let
    8.64 -  fun non_bool_eq (@{const_name "op ="}, Type (_, [T, _])) = T <> @{typ bool}
    8.65 +  fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
    8.66      | non_bool_eq _ = false;
    8.67    val hyp_subst_tac' =
    8.68      SUBGOAL (fn (goal, i) =>
    8.69 @@ -930,7 +924,7 @@
    8.70  (
    8.71    val thy = @{theory}
    8.72    type claset = Classical.claset
    8.73 -  val equality_name = @{const_name "op ="}
    8.74 +  val equality_name = @{const_name HOL.eq}
    8.75    val not_name = @{const_name Not}
    8.76    val notE = @{thm notE}
    8.77    val ccontr = @{thm ccontr}
    8.78 @@ -1746,8 +1740,8 @@
    8.79  
    8.80  fun eq_codegen thy defs dep thyname b t gr =
    8.81      (case strip_comb t of
    8.82 -       (Const (@{const_name "op ="}, Type (_, [Type ("fun", _), _])), _) => NONE
    8.83 -     | (Const (@{const_name "op ="}, _), [t, u]) =>
    8.84 +       (Const (@{const_name HOL.eq}, Type (_, [Type ("fun", _), _])), _) => NONE
    8.85 +     | (Const (@{const_name HOL.eq}, _), [t, u]) =>
    8.86            let
    8.87              val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
    8.88              val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
    8.89 @@ -1756,7 +1750,7 @@
    8.90              SOME (Codegen.parens
    8.91                (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
    8.92            end
    8.93 -     | (t as Const (@{const_name "op ="}, _), ts) => SOME (Codegen.invoke_codegen
    8.94 +     | (t as Const (@{const_name HOL.eq}, _), ts) => SOME (Codegen.invoke_codegen
    8.95           thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
    8.96       | _ => NONE);
    8.97  
    8.98 @@ -1796,7 +1790,7 @@
    8.99  
   8.100  setup {*
   8.101    Code_Preproc.map_pre (fn simpset =>
   8.102 -    simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term "op ="}]
   8.103 +    simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}]
   8.104        (fn thy => fn _ => fn Const (_, T) => case strip_type T
   8.105          of (Type _ :: _, _) => SOME @{thm eq_equal}
   8.106           | _ => NONE)])
   8.107 @@ -1944,7 +1938,7 @@
   8.108  code_const "HOL.equal"
   8.109    (Haskell infixl 4 "==")
   8.110  
   8.111 -code_const "op ="
   8.112 +code_const HOL.eq
   8.113    (Haskell infixl 4 "==")
   8.114  
   8.115  text {* undefined *}
     9.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Sat Aug 28 20:24:40 2010 +0800
     9.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Sat Aug 28 16:14:32 2010 +0200
     9.3 @@ -53,7 +53,7 @@
     9.4    F > False
     9.5    ONE_ONE > HOL4Setup.ONE_ONE
     9.6    ONTO    > Fun.surj
     9.7 -  "=" > "op ="
     9.8 +  "=" > HOL.eq
     9.9    "==>" > HOL.implies
    9.10    "/\\" > HOL.conj
    9.11    "\\/" > HOL.disj
    10.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Sat Aug 28 20:24:40 2010 +0800
    10.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Sat Aug 28 16:14:32 2010 +0200
    10.3 @@ -234,7 +234,7 @@
    10.4    ">=" > "HOLLight.hollight.>="
    10.5    ">" > "HOLLight.hollight.>"
    10.6    "==>" > HOL.implies
    10.7 -  "=" > "op ="
    10.8 +  "=" > HOL.eq
    10.9    "<=" > "HOLLight.hollight.<="
   10.10    "<" > "HOLLight.hollight.<"
   10.11    "/\\" > HOL.conj
    11.1 --- a/src/HOL/Import/hol4rews.ML	Sat Aug 28 20:24:40 2010 +0800
    11.2 +++ b/src/HOL/Import/hol4rews.ML	Sat Aug 28 16:14:32 2010 +0200
    11.3 @@ -627,7 +627,7 @@
    11.4          thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool}
    11.5              |> add_hol4_type_mapping "min" "fun" false "fun"
    11.6              |> add_hol4_type_mapping "min" "ind" false @{type_name ind}
    11.7 -            |> add_hol4_const_mapping "min" "=" false @{const_name "op ="}
    11.8 +            |> add_hol4_const_mapping "min" "=" false @{const_name HOL.eq}
    11.9              |> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies}
   11.10              |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
   11.11  in
    12.1 --- a/src/HOL/Import/proof_kernel.ML	Sat Aug 28 20:24:40 2010 +0800
    12.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Aug 28 16:14:32 2010 +0200
    12.3 @@ -1205,7 +1205,7 @@
    12.4  fun non_trivial_term_consts t = fold_aterms
    12.5    (fn Const (c, _) =>
    12.6        if c = @{const_name Trueprop} orelse c = @{const_name All}
    12.7 -        orelse c = @{const_name HOL.implies} orelse c = @{const_name HOL.conj} orelse c = @{const_name "op ="}
    12.8 +        orelse c = @{const_name HOL.implies} orelse c = @{const_name HOL.conj} orelse c = @{const_name HOL.eq}
    12.9        then I else insert (op =) c
   12.10      | _ => I) t [];
   12.11  
   12.12 @@ -1213,7 +1213,7 @@
   12.13      let
   12.14          fun add_consts (Const (c, _), cs) =
   12.15              (case c of
   12.16 -                 @{const_name "op ="} => insert (op =) "==" cs
   12.17 +                 @{const_name HOL.eq} => insert (op =) "==" cs
   12.18                 | @{const_name HOL.implies} => insert (op =) "==>" cs
   12.19                 | @{const_name All} => cs
   12.20                 | "all" => cs
   12.21 @@ -1476,10 +1476,10 @@
   12.22  fun mk_COMB th1 th2 thy =
   12.23      let
   12.24          val (f,g) = case concl_of th1 of
   12.25 -                        _ $ (Const(@{const_name "op ="},_) $ f $ g) => (f,g)
   12.26 +                        _ $ (Const(@{const_name HOL.eq},_) $ f $ g) => (f,g)
   12.27                        | _ => raise ERR "mk_COMB" "First theorem not an equality"
   12.28          val (x,y) = case concl_of th2 of
   12.29 -                        _ $ (Const(@{const_name "op ="},_) $ x $ y) => (x,y)
   12.30 +                        _ $ (Const(@{const_name HOL.eq},_) $ x $ y) => (x,y)
   12.31                        | _ => raise ERR "mk_COMB" "Second theorem not an equality"
   12.32          val fty = type_of f
   12.33          val (fd,fr) = dom_rng fty
   12.34 @@ -1788,7 +1788,7 @@
   12.35          val cv = cterm_of thy v
   12.36          val th1 = implies_elim_all (beta_eta_thm th)
   12.37          val (f,g) = case concl_of th1 of
   12.38 -                        _ $ (Const(@{const_name "op ="},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
   12.39 +                        _ $ (Const(@{const_name HOL.eq},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
   12.40                        | _ => raise ERR "mk_ABS" "Bad conclusion"
   12.41          val (fd,fr) = dom_rng (type_of f)
   12.42          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
    13.1 --- a/src/HOL/Import/shuffler.ML	Sat Aug 28 20:24:40 2010 +0800
    13.2 +++ b/src/HOL/Import/shuffler.ML	Sat Aug 28 16:14:32 2010 +0200
    13.3 @@ -60,14 +60,14 @@
    13.4  
    13.5  fun mk_meta_eq th =
    13.6      (case concl_of th of
    13.7 -         Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th RS eq_reflection
    13.8 +         Const(@{const_name Trueprop},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _) => th RS eq_reflection
    13.9         | Const("==",_) $ _ $ _ => th
   13.10         | _ => raise THM("Not an equality",0,[th]))
   13.11      handle _ => raise THM("Couldn't make meta equality",0,[th])  (* FIXME avoid handle _ *)
   13.12  
   13.13  fun mk_obj_eq th =
   13.14      (case concl_of th of
   13.15 -         Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th
   13.16 +         Const(@{const_name Trueprop},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _) => th
   13.17         | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
   13.18         | _ => raise THM("Not an equality",0,[th]))
   13.19      handle _ => raise THM("Couldn't make object equality",0,[th])  (* FIXME avoid handle _ *)
    14.1 --- a/src/HOL/Library/OptionalSugar.thy	Sat Aug 28 20:24:40 2010 +0800
    14.2 +++ b/src/HOL/Library/OptionalSugar.thy	Sat Aug 28 16:14:32 2010 +0200
    14.3 @@ -32,7 +32,7 @@
    14.4  (* deprecated, use thm with style instead, will be removed *)
    14.5  (* aligning equations *)
    14.6  notation (tab output)
    14.7 -  "op ="  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
    14.8 +  "HOL.eq"  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
    14.9    "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
   14.10  
   14.11  (* Let *)
    15.1 --- a/src/HOL/Library/reflection.ML	Sat Aug 28 20:24:40 2010 +0800
    15.2 +++ b/src/HOL/Library/reflection.ML	Sat Aug 28 16:14:32 2010 +0200
    15.3 @@ -82,7 +82,7 @@
    15.4  fun rearrange congs =
    15.5    let
    15.6      fun P (_, th) =
    15.7 -      let val @{term "Trueprop"}$(Const (@{const_name "op ="},_) $l$_) = concl_of th
    15.8 +      let val @{term "Trueprop"}$(Const (@{const_name HOL.eq},_) $l$_) = concl_of th
    15.9        in can dest_Var l end
   15.10      val (yes,no) = List.partition P congs
   15.11    in no @ yes end
    16.1 --- a/src/HOL/Mutabelle/Mutabelle.thy	Sat Aug 28 20:24:40 2010 +0800
    16.2 +++ b/src/HOL/Mutabelle/Mutabelle.thy	Sat Aug 28 16:14:32 2010 +0200
    16.3 @@ -4,7 +4,7 @@
    16.4  begin
    16.5  
    16.6  ML {*
    16.7 -val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}];
    16.8 +val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}];
    16.9  
   16.10  val forbidden =
   16.11   [(@{const_name Power.power}, "'a"),
    17.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Aug 28 20:24:40 2010 +0800
    17.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Aug 28 16:14:32 2010 +0200
    17.3 @@ -187,7 +187,7 @@
    17.4  val nitpick_mtd = ("nitpick", invoke_nitpick)
    17.5  *)
    17.6  
    17.7 -val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}]
    17.8 +val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]
    17.9  
   17.10  val forbidden =
   17.11   [(* (@{const_name "power"}, "'a"), *)
    18.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Aug 28 20:24:40 2010 +0800
    18.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Aug 28 16:14:32 2010 +0200
    18.3 @@ -183,7 +183,7 @@
    18.4    end;
    18.5  
    18.6  fun mk_not_sym ths = maps (fn th => case prop_of th of
    18.7 -    _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) => [th, th RS not_sym]
    18.8 +    _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) => [th, th RS not_sym]
    18.9    | _ => [th]) ths;
   18.10  
   18.11  fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
    19.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Sat Aug 28 20:24:40 2010 +0800
    19.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Sat Aug 28 16:14:32 2010 +0200
    19.3 @@ -147,7 +147,7 @@
    19.4               else raise EQVT_FORM "Type Implication"
    19.5            end
    19.6         (* case: eqvt-lemma is of the equational form *)
    19.7 -      | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $
    19.8 +      | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $
    19.9              (Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
   19.10             (if (apply_pi lhs (pi,typi)) = rhs
   19.11                 then [orig_thm]
    20.1 --- a/src/HOL/Set.thy	Sat Aug 28 20:24:40 2010 +0800
    20.2 +++ b/src/HOL/Set.thy	Sat Aug 28 16:14:32 2010 +0200
    20.3 @@ -268,7 +268,7 @@
    20.4  
    20.5      fun setcompr_tr [e, idts, b] =
    20.6        let
    20.7 -        val eq = Syntax.const @{const_syntax "op ="} $ Bound (nvars idts) $ e;
    20.8 +        val eq = Syntax.const @{const_syntax HOL.eq} $ Bound (nvars idts) $ e;
    20.9          val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
   20.10          val exP = ex_tr [idts, P];
   20.11        in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
   20.12 @@ -289,7 +289,7 @@
   20.13      let
   20.14        fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
   20.15          | check (Const (@{const_syntax HOL.conj}, _) $
   20.16 -              (Const (@{const_syntax "op ="}, _) $ Bound m $ e) $ P, n) =
   20.17 +              (Const (@{const_syntax HOL.eq}, _) $ Bound m $ e) $ P, n) =
   20.18              n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
   20.19              subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
   20.20          | check _ = false;
    21.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Sat Aug 28 20:24:40 2010 +0800
    21.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Sat Aug 28 16:14:32 2010 +0200
    21.3 @@ -343,7 +343,7 @@
    21.4    end handle Option => NONE)
    21.5  
    21.6  fun distinctTree_tac names ctxt 
    21.7 -      (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ x $ y)), i) =
    21.8 +      (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ x $ y)), i) =
    21.9    (case get_fst_success (neq_x_y ctxt x y) names of
   21.10       SOME neq => rtac neq i
   21.11     | NONE => no_tac)
   21.12 @@ -356,7 +356,7 @@
   21.13  
   21.14  fun distinct_simproc names =
   21.15    Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
   21.16 -    (fn thy => fn ss => fn (Const (@{const_name "op ="},_)$x$y) =>
   21.17 +    (fn thy => fn ss => fn (Const (@{const_name HOL.eq},_)$x$y) =>
   21.18          case try Simplifier.the_context ss of
   21.19          SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq]) 
   21.20                        (get_fst_success (neq_x_y ctxt x y) names)
    22.1 --- a/src/HOL/Statespace/state_fun.ML	Sat Aug 28 20:24:40 2010 +0800
    22.2 +++ b/src/HOL/Statespace/state_fun.ML	Sat Aug 28 16:14:32 2010 +0200
    22.3 @@ -285,7 +285,7 @@
    22.4                              then Bound 2
    22.5                              else raise TERM ("",[n]);
    22.6                     val sel' = lo $ d $ n' $ s;
    22.7 -                  in (Const (@{const_name "op ="},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
    22.8 +                  in (Const (@{const_name HOL.eq},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
    22.9  
   22.10           fun dest_state (s as Bound 0) = s
   22.11             | dest_state (s as (Const (sel,sT)$Bound 0)) =
   22.12 @@ -295,10 +295,10 @@
   22.13             | dest_state s = 
   22.14                      raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s]);
   22.15    
   22.16 -         fun dest_sel_eq (Const (@{const_name "op ="},Teq)$
   22.17 +         fun dest_sel_eq (Const (@{const_name HOL.eq},Teq)$
   22.18                             ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)$X) =
   22.19                             (false,Teq,lT,lo,d,n,X,dest_state s)
   22.20 -           | dest_sel_eq (Const (@{const_name "op ="},Teq)$X$
   22.21 +           | dest_sel_eq (Const (@{const_name HOL.eq},Teq)$X$
   22.22                              ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)) =
   22.23                             (true,Teq,lT,lo,d,n,X,dest_state s)
   22.24             | dest_sel_eq _ = raise TERM ("",[]);
    23.1 --- a/src/HOL/Statespace/state_space.ML	Sat Aug 28 20:24:40 2010 +0800
    23.2 +++ b/src/HOL/Statespace/state_space.ML	Sat Aug 28 16:14:32 2010 +0200
    23.3 @@ -223,7 +223,7 @@
    23.4  
    23.5  fun distinctTree_tac ctxt
    23.6        (Const (@{const_name Trueprop},_) $
    23.7 -        (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) =
    23.8 +        (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ (x as Free _)$ (y as Free _))), i) =
    23.9    (case (neq_x_y ctxt x y) of
   23.10       SOME neq => rtac neq i
   23.11     | NONE => no_tac)
   23.12 @@ -236,7 +236,7 @@
   23.13  
   23.14  val distinct_simproc =
   23.15    Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
   23.16 -    (fn thy => fn ss => (fn (Const (@{const_name "op ="},_)$(x as Free _)$(y as Free _)) =>
   23.17 +    (fn thy => fn ss => (fn (Const (@{const_name HOL.eq},_)$(x as Free _)$(y as Free _)) =>
   23.18          (case try Simplifier.the_context ss of
   23.19            SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
   23.20                         (neq_x_y ctxt x y)
    24.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sat Aug 28 20:24:40 2010 +0800
    24.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sat Aug 28 16:14:32 2010 +0200
    24.3 @@ -416,7 +416,7 @@
    24.4      fun prove_case_cong ((t, nchotomy), case_rewrites) =
    24.5        let
    24.6          val (Const ("==>", _) $ tm $ _) = t;
    24.7 -        val (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ Ma)) = tm;
    24.8 +        val (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma)) = tm;
    24.9          val cert = cterm_of thy;
   24.10          val nchotomy' = nchotomy RS spec;
   24.11          val [v] = Term.add_vars (concl_of nchotomy') [];
    25.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Sat Aug 28 20:24:40 2010 +0800
    25.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Sat Aug 28 16:14:32 2010 +0200
    25.3 @@ -96,7 +96,7 @@
    25.4          fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
    25.5            $ Free ("x", ty) $ Free ("y", ty);
    25.6          val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
    25.7 -          (mk_side @{const_name HOL.equal}, mk_side @{const_name "op ="}));
    25.8 +          (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq}));
    25.9          val def' = Syntax.check_term lthy def;
   25.10          val ((_, (_, thm)), lthy') = Specification.definition
   25.11            (NONE, (Attrib.empty_binding, def')) lthy;
    26.1 --- a/src/HOL/Tools/Function/termination.ML	Sat Aug 28 20:24:40 2010 +0800
    26.2 +++ b/src/HOL/Tools/Function/termination.ML	Sat Aug 28 16:14:32 2010 +0200
    26.3 @@ -148,7 +148,7 @@
    26.4      val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
    26.5      fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
    26.6        let
    26.7 -        val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
    26.8 +        val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
    26.9            = Term.strip_qnt_body @{const_name Ex} c
   26.10        in cons r o cons l end
   26.11    in
   26.12 @@ -185,7 +185,7 @@
   26.13      val vs = Term.strip_qnt_vars @{const_name Ex} c
   26.14  
   26.15      (* FIXME: throw error "dest_call" for malformed terms *)
   26.16 -    val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
   26.17 +    val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
   26.18        = Term.strip_qnt_body @{const_name Ex} c
   26.19      val (p, l') = dest_inj sk l
   26.20      val (q, r') = dest_inj sk r
    27.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Sat Aug 28 20:24:40 2010 +0800
    27.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Sat Aug 28 16:14:32 2010 +0200
    27.3 @@ -123,7 +123,7 @@
    27.4           Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')
    27.5         | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
    27.6           to_F Ts (t0 $ eta_expand Ts t1 1)
    27.7 -       | Const (@{const_name "op ="}, _) $ t1 $ t2 =>
    27.8 +       | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
    27.9           RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
   27.10         | Const (@{const_name ord_class.less_eq},
   27.11                  Type (@{type_name fun},
   27.12 @@ -165,8 +165,8 @@
   27.13           @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
   27.14         | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
   27.15         | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
   27.16 -       | Const (@{const_name "op ="}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
   27.17 -       | Const (@{const_name "op ="}, _) => to_R_rep Ts (eta_expand Ts t 2)
   27.18 +       | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
   27.19 +       | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
   27.20         | Const (@{const_name ord_class.less_eq},
   27.21                  Type (@{type_name fun},
   27.22                        [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
    28.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Aug 28 20:24:40 2010 +0800
    28.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Aug 28 16:14:32 2010 +0200
    28.3 @@ -408,7 +408,7 @@
    28.4     (@{const_name True}, 0),
    28.5     (@{const_name All}, 1),
    28.6     (@{const_name Ex}, 1),
    28.7 -   (@{const_name "op ="}, 1),
    28.8 +   (@{const_name HOL.eq}, 1),
    28.9     (@{const_name HOL.conj}, 2),
   28.10     (@{const_name HOL.disj}, 2),
   28.11     (@{const_name HOL.implies}, 2),
   28.12 @@ -1275,7 +1275,7 @@
   28.13          forall is_Var args andalso not (has_duplicates (op =) args)
   28.14        | _ => false
   28.15      fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
   28.16 -      | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
   28.17 +      | do_eq (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)) =
   28.18          do_lhs t1
   28.19        | do_eq _ = false
   28.20    in do_eq end
   28.21 @@ -1347,7 +1347,7 @@
   28.22      @{const "==>"} $ _ $ t2 => term_under_def t2
   28.23    | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
   28.24    | @{const Trueprop} $ t1 => term_under_def t1
   28.25 -  | Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1
   28.26 +  | Const (@{const_name HOL.eq}, _) $ t1 $ _ => term_under_def t1
   28.27    | Abs (_, _, t') => term_under_def t'
   28.28    | t1 $ _ => term_under_def t1
   28.29    | _ => t
   28.30 @@ -1371,7 +1371,7 @@
   28.31      val (lhs, rhs) =
   28.32        case t of
   28.33          Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
   28.34 -      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
   28.35 +      | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =>
   28.36          (t1, t2)
   28.37        | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
   28.38      val args = strip_comb lhs |> snd
   28.39 @@ -1453,7 +1453,7 @@
   28.40    | @{const "==>"} $ _ $ t2 => lhs_of_equation t2
   28.41    | @{const Trueprop} $ t1 => lhs_of_equation t1
   28.42    | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
   28.43 -  | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
   28.44 +  | Const (@{const_name HOL.eq}, _) $ t1 $ _ => SOME t1
   28.45    | @{const HOL.implies} $ _ $ t2 => lhs_of_equation t2
   28.46    | _ => NONE
   28.47  fun is_constr_pattern _ (Bound _) = true
   28.48 @@ -1807,7 +1807,7 @@
   28.49                          (betapply (t2, var_t))
   28.50      end
   28.51    | extensional_equal _ T t1 t2 =
   28.52 -    Const (@{const_name "op ="}, T --> T --> bool_T) $ t1 $ t2
   28.53 +    Const (@{const_name HOL.eq}, T --> T --> bool_T) $ t1 $ t2
   28.54  
   28.55  fun equationalize_term ctxt tag t =
   28.56    let
   28.57 @@ -1816,7 +1816,7 @@
   28.58    in
   28.59      Logic.list_implies (prems,
   28.60          case concl of
   28.61 -          @{const Trueprop} $ (Const (@{const_name "op ="}, Type (_, [T, _]))
   28.62 +          @{const Trueprop} $ (Const (@{const_name HOL.eq}, Type (_, [T, _]))
   28.63                                 $ t1 $ t2) =>
   28.64            @{const Trueprop} $ extensional_equal j T t1 t2
   28.65          | @{const Trueprop} $ t' =>
   28.66 @@ -2290,7 +2290,7 @@
   28.67    | simps => simps
   28.68  fun is_equational_fun_surely_complete hol_ctxt x =
   28.69    case equational_fun_axioms hol_ctxt x of
   28.70 -    [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
   28.71 +    [@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)] =>
   28.72      strip_comb t1 |> snd |> forall is_Var
   28.73    | _ => false
   28.74  
    29.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Aug 28 20:24:40 2010 +0800
    29.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Aug 28 16:14:32 2010 +0200
    29.3 @@ -590,7 +590,7 @@
    29.4                        if co then
    29.5                          Const (@{const_name The}, (T --> bool_T) --> T)
    29.6                          $ Abs (cyclic_co_val_name (), T,
    29.7 -                               Const (@{const_name "op ="}, T --> T --> bool_T)
    29.8 +                               Const (@{const_name HOL.eq}, T --> T --> bool_T)
    29.9                                 $ Bound 0 $ abstract_over (var, t))
   29.10                        else
   29.11                          cyclic_atom ()
   29.12 @@ -849,7 +849,7 @@
   29.13  (** Model reconstruction **)
   29.14  
   29.15  fun unfold_outer_the_binders (t as Const (@{const_name The}, _)
   29.16 -                                   $ Abs (s, T, Const (@{const_name "op ="}, _)
   29.17 +                                   $ Abs (s, T, Const (@{const_name HOL.eq}, _)
   29.18                                                  $ Bound 0 $ t')) =
   29.19      betapply (Abs (s, T, t'), t) |> unfold_outer_the_binders
   29.20    | unfold_outer_the_binders t = t
    30.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Aug 28 20:24:40 2010 +0800
    30.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Aug 28 16:14:32 2010 +0200
    30.3 @@ -222,7 +222,7 @@
    30.4    | fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
    30.5    | fin_fun_body dom_T ran_T
    30.6                   ((t0 as Const (@{const_name If}, _))
    30.7 -                  $ (t1 as Const (@{const_name "op ="}, _) $ Bound 0 $ t1')
    30.8 +                  $ (t1 as Const (@{const_name HOL.eq}, _) $ Bound 0 $ t1')
    30.9                    $ t2 $ t3) =
   30.10      (if loose_bvar1 (t1', 0) then
   30.11         NONE
   30.12 @@ -650,7 +650,7 @@
   30.13                                       Bound 0)))) accum
   30.14                    |>> mtype_of_mterm
   30.15                  end
   30.16 -              | @{const_name "op ="} => do_equals T accum
   30.17 +              | @{const_name HOL.eq} => do_equals T accum
   30.18                | @{const_name The} =>
   30.19                  (trace_msg (K "*** The"); raise UNSOLVABLE ())
   30.20                | @{const_name Eps} =>
   30.21 @@ -760,7 +760,7 @@
   30.22                      do_term (incr_boundvars ~1 t1') accum
   30.23                    else
   30.24                      raise SAME ()
   30.25 -                | (t11 as Const (@{const_name "op ="}, _)) $ Bound 0 $ t13 =>
   30.26 +                | (t11 as Const (@{const_name HOL.eq}, _)) $ Bound 0 $ t13 =>
   30.27                    if not (loose_bvar1 (t13, 0)) then
   30.28                      do_term (incr_boundvars ~1 (t11 $ t13)) accum
   30.29                    else
   30.30 @@ -876,7 +876,7 @@
   30.31                  do_term (@{const Not}
   30.32                           $ (HOLogic.eq_const (domain_type T0) $ t1
   30.33                              $ Abs (Name.uu, T1, @{const False}))) accum)
   30.34 -           | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
   30.35 +           | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
   30.36               do_equals x t1 t2
   30.37             | Const (@{const_name Let}, _) $ t1 $ t2 =>
   30.38               do_formula sn (betapply (t2, t1)) accum
   30.39 @@ -973,7 +973,7 @@
   30.40              do_conjunction t0 t1 t2 accum
   30.41            | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
   30.42              do_all t0 s0 T1 t1 accum
   30.43 -          | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
   30.44 +          | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
   30.45              consider_general_equals mdata true x t1 t2 accum
   30.46            | (t0 as @{const HOL.conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
   30.47            | (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
   30.48 @@ -1069,7 +1069,7 @@
   30.49                      Abs (Name.uu, set_T', @{const True})
   30.50                    | _ => Const (s, T')
   30.51                  else if s = @{const_name "=="} orelse
   30.52 -                        s = @{const_name "op ="} then
   30.53 +                        s = @{const_name HOL.eq} then
   30.54                    let
   30.55                      val T =
   30.56                        case T' of
    31.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Sat Aug 28 20:24:40 2010 +0800
    31.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Sat Aug 28 16:14:32 2010 +0200
    31.3 @@ -447,7 +447,7 @@
    31.4                  val t1 = incr_boundvars n t1
    31.5                  val t2 = incr_boundvars n t2
    31.6                  val xs = map Bound (n - 1 downto 0)
    31.7 -                val equation = Const (@{const_name "op ="},
    31.8 +                val equation = Const (@{const_name HOL.eq},
    31.9                                        body_T --> body_T --> bool_T)
   31.10                                     $ betapplys (t1, xs) $ betapplys (t2, xs)
   31.11                  val t =
   31.12 @@ -515,9 +515,9 @@
   31.13            do_description_operator The @{const_name undefined_fast_The} x t1
   31.14          | (Const (x as (@{const_name Eps}, _)), [t1]) =>
   31.15            do_description_operator Eps @{const_name undefined_fast_Eps} x t1
   31.16 -        | (Const (@{const_name "op ="}, T), [t1]) =>
   31.17 +        | (Const (@{const_name HOL.eq}, T), [t1]) =>
   31.18            Op1 (SingletonSet, range_type T, Any, sub t1)
   31.19 -        | (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2
   31.20 +        | (Const (@{const_name HOL.eq}, T), [t1, t2]) => sub_equals T t1 t2
   31.21          | (Const (@{const_name HOL.conj}, _), [t1, t2]) =>
   31.22            Op2 (And, bool_T, Any, sub' t1, sub' t2)
   31.23          | (Const (@{const_name HOL.disj}, _), [t1, t2]) =>
    32.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Sat Aug 28 20:24:40 2010 +0800
    32.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Sat Aug 28 16:14:32 2010 +0200
    32.3 @@ -41,7 +41,7 @@
    32.4      fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) =
    32.5          aux def t1 andalso aux false t2
    32.6        | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
    32.7 -      | aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) =
    32.8 +      | aux def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
    32.9          aux def t1 andalso aux false t2
   32.10        | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
   32.11        | aux def (t1 $ t2) = aux def t1 andalso aux def t2
   32.12 @@ -149,7 +149,7 @@
   32.13        case t of
   32.14          @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
   32.15        | Const (s0, _) $ t1 $ _ =>
   32.16 -        if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
   32.17 +        if s0 = @{const_name "=="} orelse s0 = @{const_name HOL.eq} then
   32.18            let
   32.19              val (t', args) = strip_comb t1
   32.20              val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
   32.21 @@ -209,7 +209,7 @@
   32.22          do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
   32.23        | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
   32.24          do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
   32.25 -      | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
   32.26 +      | Const (s0 as @{const_name HOL.eq}, T0) $ t1 $ t2 =>
   32.27          do_equals new_Ts old_Ts s0 T0 t1 t2
   32.28        | @{const HOL.conj} $ t1 $ t2 =>
   32.29          @{const HOL.conj} $ do_term new_Ts old_Ts polar t1
   32.30 @@ -332,7 +332,7 @@
   32.31          do_eq_or_imp Ts true def t0 t1 t2 seen
   32.32        | (t0 as @{const "==>"}) $ t1 $ t2 =>
   32.33          if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
   32.34 -      | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
   32.35 +      | (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
   32.36          do_eq_or_imp Ts true def t0 t1 t2 seen
   32.37        | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
   32.38          do_eq_or_imp Ts false def t0 t1 t2 seen
   32.39 @@ -399,7 +399,7 @@
   32.40          aux_eq careful true t0 t1 t2
   32.41        | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
   32.42          t0 $ aux false t1 $ aux careful t2
   32.43 -      | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
   32.44 +      | aux careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
   32.45          aux_eq careful true t0 t1 t2
   32.46        | aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
   32.47          t0 $ aux false t1 $ aux careful t2
   32.48 @@ -464,9 +464,9 @@
   32.49      and aux_implies prems zs t1 t2 =
   32.50        case t1 of
   32.51          Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
   32.52 -      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
   32.53 +      | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Var z $ t') =>
   32.54          aux_eq prems zs z t' t1 t2
   32.55 -      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
   32.56 +      | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t' $ Var z) =>
   32.57          aux_eq prems zs z t' t1 t2
   32.58        | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
   32.59      and aux_eq prems zs z t' t1 t2 =
   32.60 @@ -499,7 +499,7 @@
   32.61              handle SAME () => do_term (t :: seen) ts
   32.62          in
   32.63            case t of
   32.64 -            Const (@{const_name "op ="}, _) $ t1 $ t2 => do_eq true t1 t2
   32.65 +            Const (@{const_name HOL.eq}, _) $ t1 $ t2 => do_eq true t1 t2
   32.66            | _ => do_term (t :: seen) ts
   32.67          end
   32.68    in do_term end
   32.69 @@ -653,7 +653,7 @@
   32.70  
   32.71  fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
   32.72    | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
   32.73 -  | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
   32.74 +  | params_in_equation (Const (@{const_name HOL.eq}, _) $ t1 $ _) =
   32.75      snd (strip_comb t1)
   32.76    | params_in_equation _ = []
   32.77  
    33.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Aug 28 20:24:40 2010 +0800
    33.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Aug 28 16:14:32 2010 +0200
    33.3 @@ -179,7 +179,7 @@
    33.4  
    33.5  fun translate_literal ctxt constant_table t =
    33.6    case strip_comb t of
    33.7 -    (Const (@{const_name "op ="}, _), [l, r]) =>
    33.8 +    (Const (@{const_name HOL.eq}, _), [l, r]) =>
    33.9        let
   33.10          val l' = translate_term ctxt constant_table l
   33.11          val r' = translate_term ctxt constant_table r
    34.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Aug 28 20:24:40 2010 +0800
    34.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Aug 28 16:14:32 2010 +0200
    34.3 @@ -411,7 +411,7 @@
    34.4  fun conjuncts t = conjuncts_aux t [];
    34.5  
    34.6  fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
    34.7 -  | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true
    34.8 +  | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
    34.9    | is_equationlike_term _ = false
   34.10    
   34.11  val is_equationlike = is_equationlike_term o prop_of 
    35.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Aug 28 20:24:40 2010 +0800
    35.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Aug 28 16:14:32 2010 +0200
    35.3 @@ -587,7 +587,7 @@
    35.4  
    35.5  fun preprocess_elim ctxt elimrule =
    35.6    let
    35.7 -    fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
    35.8 +    fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, T) $ lhs $ rhs)) =
    35.9         HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
   35.10       | replace_eqs t = t
   35.11      val thy = ProofContext.theory_of ctxt
    36.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Aug 28 20:24:40 2010 +0800
    36.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Aug 28 16:14:32 2010 +0200
    36.3 @@ -111,7 +111,7 @@
    36.4  
    36.5  fun mk_meta_equation th =
    36.6    case prop_of th of
    36.7 -    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
    36.8 +    Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => th RS @{thm eq_reflection}
    36.9    | _ => th
   36.10  
   36.11  val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
   36.12 @@ -217,7 +217,7 @@
   36.13     @{const_name "==>"},
   36.14     @{const_name Trueprop},
   36.15     @{const_name Not},
   36.16 -   @{const_name "op ="},
   36.17 +   @{const_name HOL.eq},
   36.18     @{const_name HOL.implies},
   36.19     @{const_name All},
   36.20     @{const_name Ex}, 
    37.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat Aug 28 20:24:40 2010 +0800
    37.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Aug 28 16:14:32 2010 +0200
    37.3 @@ -122,8 +122,8 @@
    37.4  ( case (term_of ct) of
    37.5    Const(@{const_name HOL.conj},_)$_$_ => And (Thm.dest_binop ct)
    37.6  | Const (@{const_name HOL.disj},_)$_$_ => Or (Thm.dest_binop ct)
    37.7 -| Const (@{const_name "op ="},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
    37.8 -| Const (@{const_name Not},_) $ (Const (@{const_name "op ="},_)$y$_) =>
    37.9 +| Const (@{const_name HOL.eq},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
   37.10 +| Const (@{const_name Not},_) $ (Const (@{const_name HOL.eq},_)$y$_) =>
   37.11    if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
   37.12  | Const (@{const_name Orderings.less}, _) $ y$ z =>
   37.13     if term_of x aconv y then Lt (Thm.dest_arg ct)
   37.14 @@ -274,7 +274,7 @@
   37.15    | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
   37.16    | lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) =
   37.17      HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
   37.18 -  | lin (vs as x::_) ((b as Const(@{const_name "op ="},_))$s$t) =
   37.19 +  | lin (vs as x::_) ((b as Const(@{const_name HOL.eq},_))$s$t) =
   37.20       (case lint vs (subC$t$s) of
   37.21        (t as a$(m$c$y)$r) =>
   37.22          if x <> y then b$zero$t
   37.23 @@ -345,7 +345,7 @@
   37.24     case (term_of t) of
   37.25      Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
   37.26      if x aconv y andalso member (op =)
   37.27 -      ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   37.28 +      [@{const_name HOL.eq}, @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   37.29      then (ins (dest_number c) acc,dacc) else (acc,dacc)
   37.30    | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
   37.31      if x aconv y andalso member (op =)
   37.32 @@ -387,7 +387,7 @@
   37.33    | Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
   37.34    | Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
   37.35      if x=y andalso member (op =)
   37.36 -      ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   37.37 +      [@{const_name HOL.eq}, @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   37.38      then cv (l div dest_number c) t else Thm.reflexive t
   37.39    | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
   37.40      if x=y andalso member (op =)
    38.1 --- a/src/HOL/Tools/Qelim/qelim.ML	Sat Aug 28 20:24:40 2010 +0800
    38.2 +++ b/src/HOL/Tools/Qelim/qelim.ML	Sat Aug 28 16:14:32 2010 +0200
    38.3 @@ -26,7 +26,7 @@
    38.4      Const(s,T)$_$_ => 
    38.5         if domain_type T = HOLogic.boolT
    38.6            andalso member (op =) [@{const_name HOL.conj}, @{const_name HOL.disj},
    38.7 -            @{const_name HOL.implies}, @{const_name "op ="}] s
    38.8 +            @{const_name HOL.implies}, @{const_name HOL.eq}] s
    38.9         then binop_conv (conv env) p 
   38.10         else atcv env p
   38.11    | Const(@{const_name Not},_)$_ => arg_conv (conv env) p
    39.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 28 20:24:40 2010 +0800
    39.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 28 16:14:32 2010 +0200
    39.3 @@ -338,7 +338,7 @@
    39.4        => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
    39.5  
    39.6      (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
    39.7 -| (Const (@{const_name "op ="},_) $
    39.8 +| (Const (@{const_name HOL.eq},_) $
    39.9      (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   39.10      (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
   39.11        => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
   39.12 @@ -350,7 +350,7 @@
   39.13        => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
   39.14  
   39.15      (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
   39.16 -| Const (@{const_name "op ="},_) $
   39.17 +| Const (@{const_name HOL.eq},_) $
   39.18      (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   39.19      (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   39.20        => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
   39.21 @@ -370,13 +370,13 @@
   39.22      (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
   39.23        => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
   39.24  
   39.25 -| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
   39.26 +| Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
   39.27     (rtac @{thm refl} ORELSE'
   39.28      (equals_rsp_tac R ctxt THEN' RANGE [
   39.29         quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
   39.30  
   39.31      (* reflexivity of operators arising from Cong_tac *)
   39.32 -| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
   39.33 +| Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
   39.34  
   39.35     (* respectfulness of constants; in particular of a simple relation *)
   39.36  | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
    40.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Sat Aug 28 20:24:40 2010 +0800
    40.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sat Aug 28 16:14:32 2010 +0200
    40.3 @@ -267,7 +267,7 @@
    40.4    map_types (Envir.subst_type ty_inst) trm
    40.5  end
    40.6  
    40.7 -fun is_eq (Const (@{const_name "op ="}, _)) = true
    40.8 +fun is_eq (Const (@{const_name HOL.eq}, _)) = true
    40.9    | is_eq _ = false
   40.10  
   40.11  fun mk_rel_compose (trm1, trm2) =
   40.12 @@ -539,12 +539,12 @@
   40.13         end
   40.14  
   40.15    | (* equalities need to be replaced by appropriate equivalence relations *)
   40.16 -    (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
   40.17 +    (Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) =>
   40.18           if ty = ty' then rtrm
   40.19           else equiv_relation ctxt (domain_type ty, domain_type ty')
   40.20  
   40.21    | (* in this case we just check whether the given equivalence relation is correct *)
   40.22 -    (rel, Const (@{const_name "op ="}, ty')) =>
   40.23 +    (rel, Const (@{const_name HOL.eq}, ty')) =>
   40.24         let
   40.25           val rel_ty = fastype_of rel
   40.26           val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
   40.27 @@ -680,7 +680,7 @@
   40.28          if T = T' then rtrm
   40.29          else mk_repabs ctxt (T, T') rtrm
   40.30  
   40.31 -  | (_, Const (@{const_name "op ="}, _)) => rtrm
   40.32 +  | (_, Const (@{const_name HOL.eq}, _)) => rtrm
   40.33  
   40.34    | (_, Const (_, T')) =>
   40.35        let
    41.1 --- a/src/HOL/Tools/SMT/smt_monomorph.ML	Sat Aug 28 20:24:40 2010 +0800
    41.2 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Sat Aug 28 16:14:32 2010 +0200
    41.3 @@ -16,7 +16,7 @@
    41.4  
    41.5  val ignored = member (op =) [
    41.6    @{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If},
    41.7 -  @{const_name "op ="}, @{const_name zero_class.zero},
    41.8 +  @{const_name HOL.eq}, @{const_name zero_class.zero},
    41.9    @{const_name one_class.one}, @{const_name number_of}]
   41.10  
   41.11  fun is_const f (n, T) = not (ignored n) andalso f T
    42.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Sat Aug 28 20:24:40 2010 +0800
    42.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Sat Aug 28 16:14:32 2010 +0200
    42.3 @@ -252,7 +252,7 @@
    42.4  
    42.5  fun norm_def ctxt thm =
    42.6    (case Thm.prop_of thm of
    42.7 -    @{term Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ Abs _) =>
    42.8 +    @{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
    42.9        norm_def ctxt (thm RS @{thm fun_cong})
   42.10    | Const (@{const_name "=="}, _) $ _ $ Abs _ =>
   42.11        norm_def ctxt (thm RS @{thm meta_eq_to_obj_eq})
    43.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Sat Aug 28 20:24:40 2010 +0800
    43.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Sat Aug 28 16:14:32 2010 +0200
    43.3 @@ -162,12 +162,12 @@
    43.4    | conn @{const_name HOL.conj} = SOME "and"
    43.5    | conn @{const_name HOL.disj} = SOME "or"
    43.6    | conn @{const_name HOL.implies} = SOME "implies"
    43.7 -  | conn @{const_name "op ="} = SOME "iff"
    43.8 +  | conn @{const_name HOL.eq} = SOME "iff"
    43.9    | conn @{const_name If} = SOME "if_then_else"
   43.10    | conn _ = NONE
   43.11  
   43.12  fun pred @{const_name distinct} _ = SOME "distinct"
   43.13 -  | pred @{const_name "op ="} _ = SOME "="
   43.14 +  | pred @{const_name HOL.eq} _ = SOME "="
   43.15    | pred @{const_name term_eq} _ = SOME "="
   43.16    | pred @{const_name less} T = if_int_type T "<"
   43.17    | pred @{const_name less_eq} T = if_int_type T "<="
    44.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Sat Aug 28 20:24:40 2010 +0800
    44.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Sat Aug 28 16:14:32 2010 +0200
    44.3 @@ -176,7 +176,7 @@
    44.4  fun mk_nary _ cu [] = cu
    44.5    | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
    44.6  
    44.7 -val eq = mk_inst_pair destT1 @{cpat "op ="}
    44.8 +val eq = mk_inst_pair destT1 @{cpat HOL.eq}
    44.9  fun mk_eq ct cu = Thm.mk_binop (instT' ct eq) ct cu
   44.10  
   44.11  val if_term = mk_inst_pair (destT1 o destT2) @{cpat If}
    45.1 --- a/src/HOL/Tools/SMT/z3_proof_literals.ML	Sat Aug 28 20:24:40 2010 +0800
    45.2 +++ b/src/HOL/Tools/SMT/z3_proof_literals.ML	Sat Aug 28 16:14:32 2010 +0200
    45.3 @@ -234,7 +234,7 @@
    45.4          @{term Not} $ (@{term Not} $ t) => (T.compose dnegI, lookup t)
    45.5        | @{term Not} $ (@{term "op = :: bool => _"} $ t $ (@{term Not} $ u)) =>
    45.6            (T.compose negIffI, lookup (iff_const $ u $ t))
    45.7 -      | @{term Not} $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u) =>
    45.8 +      | @{term Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
    45.9            let fun rewr lit = lit COMP @{thm not_sym}
   45.10            in (rewr, lookup (@{term Not} $ (eq $ u $ t))) end
   45.11        | _ =>
    46.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Sat Aug 28 20:24:40 2010 +0800
    46.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Sat Aug 28 16:14:32 2010 +0200
    46.3 @@ -199,7 +199,7 @@
    46.4        | @{term HOL.conj} $ _ $ _ => abstr2 cvs ct
    46.5        | @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
    46.6        | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
    46.7 -      | Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
    46.8 +      | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
    46.9        | Const (@{const_name distinct}, _) $ _ =>
   46.10            if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
   46.11            else fresh_abstraction cvs ct
    47.1 --- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Sat Aug 28 20:24:40 2010 +0800
    47.2 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Sat Aug 28 16:14:32 2010 +0200
    47.3 @@ -83,7 +83,7 @@
    47.4     (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
    47.5  fun extensionalize_theorem th =
    47.6    case prop_of th of
    47.7 -    _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
    47.8 +    _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _]))
    47.9           $ _ $ Abs (s, _, _)) => extensionalize_theorem (th RS fun_cong_all)
   47.10    | _ => th
   47.11  
    48.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Sat Aug 28 20:24:40 2010 +0800
    48.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Sat Aug 28 16:14:32 2010 +0200
    48.3 @@ -94,7 +94,7 @@
    48.4  val const_trans_table =
    48.5    Symtab.make [(@{type_name Product_Type.prod}, "prod"),
    48.6                 (@{type_name Sum_Type.sum}, "sum"),
    48.7 -               (@{const_name "op ="}, "equal"),
    48.8 +               (@{const_name HOL.eq}, "equal"),
    48.9                 (@{const_name HOL.conj}, "and"),
   48.10                 (@{const_name HOL.disj}, "or"),
   48.11                 (@{const_name HOL.implies}, "implies"),
   48.12 @@ -111,7 +111,7 @@
   48.13  
   48.14  (* Invert the table of translations between Isabelle and ATPs. *)
   48.15  val const_trans_table_inv =
   48.16 -  Symtab.update ("fequal", @{const_name "op ="})
   48.17 +  Symtab.update ("fequal", @{const_name HOL.eq})
   48.18                  (Symtab.make (map swap (Symtab.dest const_trans_table)))
   48.19  
   48.20  val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
   48.21 @@ -185,8 +185,8 @@
   48.22      SOME c' => c'
   48.23    | NONE => ascii_of c
   48.24  
   48.25 -(* "op =" MUST BE "equal" because it's built into ATPs. *)
   48.26 -fun make_fixed_const @{const_name "op ="} = "equal"
   48.27 +(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
   48.28 +fun make_fixed_const @{const_name HOL.eq} = "equal"
   48.29    | make_fixed_const c = const_prefix ^ lookup_const c
   48.30  
   48.31  fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
    49.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Sat Aug 28 20:24:40 2010 +0800
    49.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Sat Aug 28 16:14:32 2010 +0200
    49.3 @@ -224,7 +224,7 @@
    49.4  
    49.5  fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
    49.6  
    49.7 -fun smart_invert_const "fequal" = @{const_name "op ="}
    49.8 +fun smart_invert_const "fequal" = @{const_name HOL.eq}
    49.9    | smart_invert_const s = invert_const s
   49.10  
   49.11  fun hol_type_from_metis_term _ (Metis.Term.Var v) =
   49.12 @@ -264,7 +264,7 @@
   49.13              end
   49.14          | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
   49.15        and applic_to_tt ("=",ts) =
   49.16 -            Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
   49.17 +            Term (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
   49.18          | applic_to_tt (a,ts) =
   49.19              case strip_prefix_and_unascii const_prefix a of
   49.20                  SOME b =>
   49.21 @@ -311,7 +311,7 @@
   49.22                    SOME w =>  mk_var(w, dummyT)
   49.23                  | NONE   => mk_var(v, dummyT))
   49.24          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
   49.25 -            Const (@{const_name "op ="}, HOLogic.typeT)
   49.26 +            Const (@{const_name HOL.eq}, HOLogic.typeT)
   49.27          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
   49.28             (case strip_prefix_and_unascii const_prefix x of
   49.29                  SOME c => Const (smart_invert_const c, dummyT)
   49.30 @@ -325,7 +325,7 @@
   49.31              cvt tm1 $ cvt tm2
   49.32          | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
   49.33          | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
   49.34 -            list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
   49.35 +            list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
   49.36          | cvt (t as Metis.Term.Fn (x, [])) =
   49.37             (case strip_prefix_and_unascii const_prefix x of
   49.38                  SOME c => Const (smart_invert_const c, dummyT)
   49.39 @@ -480,7 +480,7 @@
   49.40        val c_t = cterm_incr_types thy refl_idx i_t
   49.41    in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   49.42  
   49.43 -fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0  (*equality has no type arguments*)
   49.44 +fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0  (*equality has no type arguments*)
   49.45    | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
   49.46    | get_ty_arg_size _ _ = 0;
   49.47  
   49.48 @@ -529,13 +529,13 @@
   49.49                        " isa-term: " ^  Syntax.string_of_term ctxt tm ^
   49.50                        " fol-term: " ^ Metis.Term.toString t)
   49.51        fun path_finder FO tm ps _ = path_finder_FO tm ps
   49.52 -        | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
   49.53 +        | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
   49.54               (*equality: not curried, as other predicates are*)
   49.55               if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
   49.56               else path_finder_HO tm (p::ps)        (*1 selects second operand*)
   49.57          | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
   49.58               path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
   49.59 -        | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
   49.60 +        | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
   49.61                              (Metis.Term.Fn ("=", [t1,t2])) =
   49.62               (*equality: not curried, as other predicates are*)
   49.63               if p=0 then path_finder_FT tm (0::1::ps)
    50.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Sat Aug 28 20:24:40 2010 +0800
    50.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Sat Aug 28 16:14:32 2010 +0200
    50.3 @@ -121,7 +121,7 @@
    50.4     handled specially via "fequal". *)
    50.5  val boring_consts =
    50.6    [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
    50.7 -   @{const_name "op ="}]
    50.8 +   @{const_name HOL.eq}]
    50.9  
   50.10  (* Add a pconstant to the table, but a [] entry means a standard
   50.11     connective, which we ignore.*)
   50.12 @@ -177,7 +177,7 @@
   50.13        | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
   50.14        | @{const HOL.implies} $ t1 $ t2 =>
   50.15          do_formula (flip pos) t1 #> do_formula pos t2
   50.16 -      | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
   50.17 +      | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
   50.18          fold (do_term_or_formula T) [t1, t2]
   50.19        | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
   50.20          $ t1 $ t2 $ t3 =>
   50.21 @@ -557,7 +557,7 @@
   50.22        | (_, @{const Not} $ t1) => do_formula (not pos) t1
   50.23        | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
   50.24        | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
   50.25 -      | (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2
   50.26 +      | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
   50.27        | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
   50.28        | _ => false
   50.29    in do_formula true end
    51.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Sat Aug 28 20:24:40 2010 +0800
    51.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Sat Aug 28 16:14:32 2010 +0200
    51.3 @@ -315,7 +315,7 @@
    51.4            | _ => raise FO_TERM us
    51.5          else case strip_prefix_and_unascii const_prefix a of
    51.6            SOME "equal" =>
    51.7 -          list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
    51.8 +          list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT),
    51.9                       map (aux NONE []) us)
   51.10          | SOME b =>
   51.11            let
   51.12 @@ -527,7 +527,7 @@
   51.13    | is_bad_free _ _ = false
   51.14  
   51.15  (* Vampire is keen on producing these. *)
   51.16 -fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _)
   51.17 +fun is_trivial_formula (@{const Not} $ (Const (@{const_name HOL.eq}, _)
   51.18                                          $ t1 $ t2)) = (t1 aconv t2)
   51.19    | is_trivial_formula _ = false
   51.20  
    52.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Sat Aug 28 20:24:40 2010 +0800
    52.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Sat Aug 28 16:14:32 2010 +0200
    52.3 @@ -73,7 +73,7 @@
    52.4        | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
    52.5        | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
    52.6        | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
    52.7 -      | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
    52.8 +      | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
    52.9          do_conn bs AIff t1 t2
   52.10        | _ => (fn ts => do_term bs (Envir.eta_contract t)
   52.11                         |>> AAtom ||> union (op =) ts)
   52.12 @@ -97,7 +97,7 @@
   52.13        | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
   52.14                                          Type (_, [_, res_T])]))
   52.15                      $ t2 $ Abs (var_s, var_T, t')) =
   52.16 -        if s = @{const_name "op ="} orelse s = @{const_name "=="} then
   52.17 +        if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
   52.18            let val var_t = Var ((var_s, j), var_T) in
   52.19              Const (s, T' --> T' --> res_T)
   52.20                $ betapply (t2, var_t) $ subst_bound (var_t, t')
   52.21 @@ -128,7 +128,7 @@
   52.22            | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   52.23            | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   52.24            | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   52.25 -          | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
   52.26 +          | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
   52.27                $ t1 $ t2 =>
   52.28              t0 $ aux Ts t1 $ aux Ts t2
   52.29            | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
    53.1 --- a/src/HOL/Tools/TFL/dcterm.ML	Sat Aug 28 20:24:40 2010 +0800
    53.2 +++ b/src/HOL/Tools/TFL/dcterm.ML	Sat Aug 28 16:14:32 2010 +0200
    53.3 @@ -127,7 +127,7 @@
    53.4  
    53.5  val dest_neg    = dest_monop @{const_name Not}
    53.6  val dest_pair   = dest_binop @{const_name Pair}
    53.7 -val dest_eq     = dest_binop @{const_name "op ="}
    53.8 +val dest_eq     = dest_binop @{const_name HOL.eq}
    53.9  val dest_imp    = dest_binop @{const_name HOL.implies}
   53.10  val dest_conj   = dest_binop @{const_name HOL.conj}
   53.11  val dest_disj   = dest_binop @{const_name HOL.disj}
    54.1 --- a/src/HOL/Tools/TFL/post.ML	Sat Aug 28 20:24:40 2010 +0800
    54.2 +++ b/src/HOL/Tools/TFL/post.ML	Sat Aug 28 16:14:32 2010 +0200
    54.3 @@ -67,7 +67,7 @@
    54.4  val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
    54.5  fun mk_meta_eq r = case concl_of r of
    54.6       Const("==",_)$_$_ => r
    54.7 -  |   _ $(Const(@{const_name "op ="},_)$_$_) => r RS eq_reflection
    54.8 +  |   _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection
    54.9    |   _ => r RS P_imp_P_eq_True
   54.10  
   54.11  (*Is this the best way to invoke the simplifier??*)
    55.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Sat Aug 28 20:24:40 2010 +0800
    55.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Sat Aug 28 16:14:32 2010 +0200
    55.3 @@ -244,7 +244,7 @@
    55.4       end
    55.5    | dest_abs _ _ =  raise USYN_ERR "dest_abs" "not an abstraction";
    55.6  
    55.7 -fun dest_eq(Const(@{const_name "op ="},_) $ M $ N) = {lhs=M, rhs=N}
    55.8 +fun dest_eq(Const(@{const_name HOL.eq},_) $ M $ N) = {lhs=M, rhs=N}
    55.9    | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
   55.10  
   55.11  fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N}
    56.1 --- a/src/HOL/Tools/cnf_funcs.ML	Sat Aug 28 20:24:40 2010 +0800
    56.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Sat Aug 28 16:14:32 2010 +0200
    56.3 @@ -98,7 +98,7 @@
    56.4    | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _)                                    = false
    56.5    | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _)                                    = false
    56.6    | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _)                                  = false
    56.7 -  | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _)       = false
    56.8 +  | is_atom (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ _ $ _)       = false
    56.9    | is_atom (Const (@{const_name Not}, _) $ _)                                         = false
   56.10    | is_atom _                                                              = true;
   56.11  
   56.12 @@ -205,7 +205,7 @@
   56.13  	in
   56.14  		make_nnf_imp OF [thm1, thm2]
   56.15  	end
   56.16 -  | make_nnf_thm thy (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
   56.17 +  | make_nnf_thm thy (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
   56.18  	let
   56.19  		val thm1 = make_nnf_thm thy x
   56.20  		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
   56.21 @@ -239,7 +239,7 @@
   56.22  	in
   56.23  		make_nnf_not_imp OF [thm1, thm2]
   56.24  	end
   56.25 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
   56.26 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
   56.27  	let
   56.28  		val thm1 = make_nnf_thm thy x
   56.29  		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
    57.1 --- a/src/HOL/Tools/groebner.ML	Sat Aug 28 20:24:40 2010 +0800
    57.2 +++ b/src/HOL/Tools/groebner.ML	Sat Aug 28 16:14:32 2010 +0200
    57.3 @@ -409,7 +409,7 @@
    57.4      | _  => false;
    57.5  fun is_eq t =
    57.6   case term_of t of
    57.7 - (Const(@{const_name "op ="},_)$_$_) => true
    57.8 + (Const(@{const_name HOL.eq},_)$_$_) => true
    57.9  | _  => false;
   57.10  
   57.11  fun end_itlist f l =
   57.12 @@ -923,7 +923,7 @@
   57.13  
   57.14  fun find_term bounds tm =
   57.15    (case term_of tm of
   57.16 -    Const (@{const_name "op ="}, T) $ _ $ _ =>
   57.17 +    Const (@{const_name HOL.eq}, T) $ _ $ _ =>
   57.18        if domain_type T = HOLogic.boolT then find_args bounds tm
   57.19        else dest_arg tm
   57.20    | Const (@{const_name Not}, _) $ _ => find_term bounds (dest_arg tm)
   57.21 @@ -985,7 +985,7 @@
   57.22  
   57.23  local
   57.24   fun lhs t = case term_of t of
   57.25 -  Const(@{const_name "op ="},_)$_$_ => Thm.dest_arg1 t
   57.26 +  Const(@{const_name HOL.eq},_)$_$_ => Thm.dest_arg1 t
   57.27   | _=> raise CTERM ("ideal_tac - lhs",[t])
   57.28   fun exitac NONE = no_tac
   57.29     | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
    58.1 --- a/src/HOL/Tools/hologic.ML	Sat Aug 28 20:24:40 2010 +0800
    58.2 +++ b/src/HOL/Tools/hologic.ML	Sat Aug 28 16:14:32 2010 +0200
    58.3 @@ -236,10 +236,10 @@
    58.4  fun dest_not (Const ("HOL.Not", _) $ t) = t
    58.5    | dest_not t = raise TERM ("dest_not", [t]);
    58.6  
    58.7 -fun eq_const T = Const ("op =", T --> T --> boolT);
    58.8 +fun eq_const T = Const ("HOL.eq", T --> T --> boolT);
    58.9  fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
   58.10  
   58.11 -fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
   58.12 +fun dest_eq (Const ("HOL.eq", _) $ lhs $ rhs) = (lhs, rhs)
   58.13    | dest_eq t = raise TERM ("dest_eq", [t])
   58.14  
   58.15  fun all_const T = Const ("HOL.All", [T --> boolT] ---> boolT);
    59.1 --- a/src/HOL/Tools/inductive.ML	Sat Aug 28 20:24:40 2010 +0800
    59.2 +++ b/src/HOL/Tools/inductive.ML	Sat Aug 28 16:14:32 2010 +0200
    59.3 @@ -182,7 +182,7 @@
    59.4    in
    59.5      case concl_of thm of
    59.6        Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
    59.7 -    | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => eq2mono thm
    59.8 +    | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq2mono thm
    59.9      | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
   59.10        dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
   59.11          (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
    60.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sat Aug 28 20:24:40 2010 +0800
    60.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sat Aug 28 16:14:32 2010 +0200
    60.3 @@ -52,7 +52,7 @@
    60.4      fun thyname_of s = (case optmod of
    60.5        NONE => Codegen.thyname_of_const thy s | SOME s => s);
    60.6    in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of
    60.7 -      SOME (Const (@{const_name "op ="}, _), [t, _]) =>
    60.8 +      SOME (Const (@{const_name HOL.eq}, _), [t, _]) =>
    60.9          (case head_of t of
   60.10            Const (s, _) =>
   60.11              CodegenData.put {intros = intros, graph = graph,
   60.12 @@ -188,7 +188,7 @@
   60.13          end)) (AList.lookup op = modes name)
   60.14  
   60.15    in (case strip_comb t of
   60.16 -      (Const (@{const_name "op ="}, Type (_, [T, _])), _) =>
   60.17 +      (Const (@{const_name HOL.eq}, Type (_, [T, _])), _) =>
   60.18          [Mode ((([], [1]), false), [1], []), Mode ((([], [2]), false), [2], [])] @
   60.19          (if is_eqT T then [Mode ((([], [1, 2]), false), [1, 2], [])] else [])
   60.20      | (Const (name, _), args) => the_default default (mk_modes name args)
   60.21 @@ -344,7 +344,7 @@
   60.22    end;
   60.23  
   60.24  fun modename module s (iss, is) gr =
   60.25 -  let val (id, gr') = if s = @{const_name "op ="} then (("", "equal"), gr)
   60.26 +  let val (id, gr') = if s = @{const_name HOL.eq} then (("", "equal"), gr)
   60.27      else mk_const_id module s gr
   60.28    in (space_implode "__"
   60.29      (mk_qual_id module id ::
   60.30 @@ -363,7 +363,7 @@
   60.31    | compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr =
   60.32        (case strip_comb t of
   60.33           (Const (name, _), args) =>
   60.34 -           if name = @{const_name "op ="} orelse AList.defined op = modes name then
   60.35 +           if name = @{const_name HOL.eq} orelse AList.defined op = modes name then
   60.36               let
   60.37                 val (args1, args2) = chop (length ms) args;
   60.38                 val ((ps, mode_id), gr') = gr |> fold_map
   60.39 @@ -581,7 +581,7 @@
   60.40  
   60.41        fun dest_prem (_ $ (Const (@{const_name Set.member}, _) $ t $ u)) =
   60.42              Prem ([t], Envir.beta_eta_contract u, true)
   60.43 -        | dest_prem (_ $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u)) =
   60.44 +        | dest_prem (_ $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u)) =
   60.45              Prem ([t, u], eq, false)
   60.46          | dest_prem (_ $ t) =
   60.47              (case strip_comb t of
    61.1 --- a/src/HOL/Tools/inductive_set.ML	Sat Aug 28 20:24:40 2010 +0800
    61.2 +++ b/src/HOL/Tools/inductive_set.ML	Sat Aug 28 16:14:32 2010 +0200
    61.3 @@ -265,7 +265,7 @@
    61.4  
    61.5  fun add ctxt thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
    61.6    case prop_of thm of
    61.7 -    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, Type (_, [T, _])) $ lhs $ rhs) =>
    61.8 +    Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ lhs $ rhs) =>
    61.9        (case body_type T of
   61.10           @{typ bool} =>
   61.11             let
    62.1 --- a/src/HOL/Tools/int_arith.ML	Sat Aug 28 20:24:40 2010 +0800
    62.2 +++ b/src/HOL/Tools/int_arith.ML	Sat Aug 28 16:14:32 2010 +0200
    62.3 @@ -51,7 +51,7 @@
    62.4  
    62.5  fun check (Const (@{const_name Groups.one}, @{typ int})) = false
    62.6    | check (Const (@{const_name Groups.one}, _)) = true
    62.7 -  | check (Const (s, _)) = member (op =) [@{const_name "op ="},
    62.8 +  | check (Const (s, _)) = member (op =) [@{const_name HOL.eq},
    62.9        @{const_name Groups.times}, @{const_name Groups.uminus},
   62.10        @{const_name Groups.minus}, @{const_name Groups.plus},
   62.11        @{const_name Groups.zero},
    63.1 --- a/src/HOL/Tools/lin_arith.ML	Sat Aug 28 20:24:40 2010 +0800
    63.2 +++ b/src/HOL/Tools/lin_arith.ML	Sat Aug 28 16:14:32 2010 +0200
    63.3 @@ -229,7 +229,7 @@
    63.4    case rel of
    63.5      @{const_name Orderings.less}    => SOME (p, i, "<", q, j)
    63.6    | @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j)
    63.7 -  | "op ="              => SOME (p, i, "=", q, j)
    63.8 +  | @{const_name HOL.eq}            => SOME (p, i, "=", q, j)
    63.9    | _                   => NONE
   63.10  end handle Rat.DIVZERO => NONE;
   63.11  
   63.12 @@ -427,7 +427,7 @@
   63.13          val t2'             = incr_boundvars 1 t2
   63.14          val t1_lt_t2        = Const (@{const_name Orderings.less},
   63.15                                  split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   63.16 -        val t1_eq_t2_plus_d = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   63.17 +        val t1_eq_t2_plus_d = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   63.18                                  (Const (@{const_name Groups.plus},
   63.19                                    split_type --> split_type --> split_type) $ t2' $ d)
   63.20          val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   63.21 @@ -447,7 +447,7 @@
   63.22                              (map (incr_boundvars 1) rev_terms)
   63.23          val terms2      = map (subst_term [(split_term, zero_nat)]) rev_terms
   63.24          val t1'         = incr_boundvars 1 t1
   63.25 -        val t1_eq_nat_n = Const (@{const_name "op ="}, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
   63.26 +        val t1_eq_nat_n = Const (@{const_name HOL.eq}, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
   63.27                              (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
   63.28          val t1_lt_zero  = Const (@{const_name Orderings.less},
   63.29                              HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
   63.30 @@ -471,13 +471,13 @@
   63.31                                          (map (incr_boundvars 2) rev_terms)
   63.32          val t1'                     = incr_boundvars 2 t1
   63.33          val t2'                     = incr_boundvars 2 t2
   63.34 -        val t2_eq_zero              = Const (@{const_name "op ="},
   63.35 +        val t2_eq_zero              = Const (@{const_name HOL.eq},
   63.36                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   63.37 -        val t2_neq_zero             = HOLogic.mk_not (Const (@{const_name "op ="},
   63.38 +        val t2_neq_zero             = HOLogic.mk_not (Const (@{const_name HOL.eq},
   63.39                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
   63.40          val j_lt_t2                 = Const (@{const_name Orderings.less},
   63.41                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   63.42 -        val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   63.43 +        val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   63.44                                         (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
   63.45                                           (Const (@{const_name Groups.times},
   63.46                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
   63.47 @@ -503,13 +503,13 @@
   63.48                                          (map (incr_boundvars 2) rev_terms)
   63.49          val t1'                     = incr_boundvars 2 t1
   63.50          val t2'                     = incr_boundvars 2 t2
   63.51 -        val t2_eq_zero              = Const (@{const_name "op ="},
   63.52 +        val t2_eq_zero              = Const (@{const_name HOL.eq},
   63.53                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   63.54 -        val t2_neq_zero             = HOLogic.mk_not (Const (@{const_name "op ="},
   63.55 +        val t2_neq_zero             = HOLogic.mk_not (Const (@{const_name HOL.eq},
   63.56                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
   63.57          val j_lt_t2                 = Const (@{const_name Orderings.less},
   63.58                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   63.59 -        val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   63.60 +        val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   63.61                                         (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
   63.62                                           (Const (@{const_name Groups.times},
   63.63                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
   63.64 @@ -541,7 +541,7 @@
   63.65                                          (map (incr_boundvars 2) rev_terms)
   63.66          val t1'                     = incr_boundvars 2 t1
   63.67          val t2'                     = incr_boundvars 2 t2
   63.68 -        val t2_eq_zero              = Const (@{const_name "op ="},
   63.69 +        val t2_eq_zero              = Const (@{const_name HOL.eq},
   63.70                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   63.71          val zero_lt_t2              = Const (@{const_name Orderings.less},
   63.72                                          split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
   63.73 @@ -555,7 +555,7 @@
   63.74                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   63.75          val t2_lt_j                 = Const (@{const_name Orderings.less},
   63.76                                          split_type --> split_type--> HOLogic.boolT) $ t2' $ j
   63.77 -        val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   63.78 +        val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   63.79                                         (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
   63.80                                           (Const (@{const_name Groups.times},
   63.81                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
   63.82 @@ -595,7 +595,7 @@
   63.83                                          (map (incr_boundvars 2) rev_terms)
   63.84          val t1'                     = incr_boundvars 2 t1
   63.85          val t2'                     = incr_boundvars 2 t2
   63.86 -        val t2_eq_zero              = Const (@{const_name "op ="},
   63.87 +        val t2_eq_zero              = Const (@{const_name HOL.eq},
   63.88                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   63.89          val zero_lt_t2              = Const (@{const_name Orderings.less},
   63.90                                          split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
   63.91 @@ -609,7 +609,7 @@
   63.92                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   63.93          val t2_lt_j                 = Const (@{const_name Orderings.less},
   63.94                                          split_type --> split_type--> HOLogic.boolT) $ t2' $ j
   63.95 -        val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   63.96 +        val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   63.97                                         (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
   63.98                                           (Const (@{const_name Groups.times},
   63.99                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
    64.1 --- a/src/HOL/Tools/meson.ML	Sat Aug 28 20:24:40 2010 +0800
    64.2 +++ b/src/HOL/Tools/meson.ML	Sat Aug 28 16:14:32 2010 +0200
    64.3 @@ -183,7 +183,7 @@
    64.4  fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
    64.5  
    64.6  (*Literals like X=X are tautologous*)
    64.7 -fun taut_poslit (Const(@{const_name "op ="},_) $ t $ u) = t aconv u
    64.8 +fun taut_poslit (Const(@{const_name HOL.eq},_) $ t $ u) = t aconv u
    64.9    | taut_poslit (Const(@{const_name True},_)) = true
   64.10    | taut_poslit _ = false;
   64.11  
   64.12 @@ -213,7 +213,7 @@
   64.13         case HOLogic.dest_Trueprop (concl_of th) of
   64.14            (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) =>
   64.15              refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
   64.16 -        | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
   64.17 +        | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ t $ u)) $ _) =>
   64.18              if eliminable(t,u)
   64.19              then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
   64.20              else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
   64.21 @@ -222,7 +222,7 @@
   64.22  
   64.23  fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) =
   64.24        notequal_lits_count P + notequal_lits_count Q
   64.25 -  | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
   64.26 +  | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _)) = 1
   64.27    | notequal_lits_count _ = 0;
   64.28  
   64.29  (*Simplify a clause by applying reflexivity to its negated equality literals*)
   64.30 @@ -280,7 +280,7 @@
   64.31      | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
   64.32          if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
   64.33               else sum (signed_nclauses (not b) t) (signed_nclauses b u)
   64.34 -    | signed_nclauses b (Const(@{const_name "op ="}, Type ("fun", [T, _])) $ t $ u) =
   64.35 +    | signed_nclauses b (Const(@{const_name HOL.eq}, Type ("fun", [T, _])) $ t $ u) =
   64.36          if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
   64.37              if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
   64.38                            (prod (signed_nclauses (not b) u) (signed_nclauses b t))
    65.1 --- a/src/HOL/Tools/nat_arith.ML	Sat Aug 28 20:24:40 2010 +0800
    65.2 +++ b/src/HOL/Tools/nat_arith.ML	Sat Aug 28 16:14:32 2010 +0200
    65.3 @@ -62,7 +62,7 @@
    65.4  (struct
    65.5    open CommonCancelSums;
    65.6    val mk_bal = HOLogic.mk_eq;
    65.7 -  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
    65.8 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT;
    65.9    val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
   65.10  end);
   65.11  
    66.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Aug 28 20:24:40 2010 +0800
    66.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Aug 28 16:14:32 2010 +0200
    66.3 @@ -168,7 +168,7 @@
    66.4   (open CancelNumeralsCommon
    66.5    val prove_conv = Arith_Data.prove_conv
    66.6    val mk_bal   = HOLogic.mk_eq
    66.7 -  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
    66.8 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
    66.9    val bal_add1 = @{thm nat_eq_add_iff1} RS trans
   66.10    val bal_add2 = @{thm nat_eq_add_iff2} RS trans
   66.11  );
   66.12 @@ -300,7 +300,7 @@
   66.13   (open CancelNumeralFactorCommon
   66.14    val prove_conv = Arith_Data.prove_conv
   66.15    val mk_bal   = HOLogic.mk_eq
   66.16 -  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   66.17 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
   66.18    val cancel = @{thm nat_mult_eq_cancel1} RS trans
   66.19    val neg_exchanges = false
   66.20  )
   66.21 @@ -380,7 +380,7 @@
   66.22   (open CancelFactorCommon
   66.23    val prove_conv = Arith_Data.prove_conv
   66.24    val mk_bal   = HOLogic.mk_eq
   66.25 -  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   66.26 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
   66.27    fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj}
   66.28  );
   66.29  
    67.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Sat Aug 28 20:24:40 2010 +0800
    67.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Aug 28 16:14:32 2010 +0200
    67.3 @@ -222,7 +222,7 @@
    67.4   (open CancelNumeralsCommon
    67.5    val prove_conv = Arith_Data.prove_conv
    67.6    val mk_bal   = HOLogic.mk_eq
    67.7 -  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    67.8 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
    67.9    val bal_add1 = @{thm eq_add_iff1} RS trans
   67.10    val bal_add2 = @{thm eq_add_iff2} RS trans
   67.11  );
   67.12 @@ -401,7 +401,7 @@
   67.13   (open CancelNumeralFactorCommon
   67.14    val prove_conv = Arith_Data.prove_conv
   67.15    val mk_bal   = HOLogic.mk_eq
   67.16 -  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   67.17 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
   67.18    val cancel = @{thm mult_cancel_left} RS trans
   67.19    val neg_exchanges = false
   67.20  )
   67.21 @@ -516,7 +516,7 @@
   67.22   (open CancelFactorCommon
   67.23    val prove_conv = Arith_Data.prove_conv
   67.24    val mk_bal   = HOLogic.mk_eq
   67.25 -  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   67.26 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
   67.27    fun simp_conv _ _ = SOME @{thm mult_cancel_left}
   67.28  );
   67.29  
   67.30 @@ -606,7 +606,7 @@
   67.31  local
   67.32   val zr = @{cpat "0"}
   67.33   val zT = ctyp_of_term zr
   67.34 - val geq = @{cpat "op ="}
   67.35 + val geq = @{cpat HOL.eq}
   67.36   val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
   67.37   val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
   67.38   val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
   67.39 @@ -676,7 +676,7 @@
   67.40          val T = ctyp_of_term c
   67.41          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
   67.42        in SOME (mk_meta_eq th) end
   67.43 -  | Const(@{const_name "op ="},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
   67.44 +  | Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
   67.45        let
   67.46          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   67.47          val _ = map is_number [a,b,c]
   67.48 @@ -697,7 +697,7 @@
   67.49          val T = ctyp_of_term c
   67.50          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
   67.51        in SOME (mk_meta_eq th) end
   67.52 -  | Const(@{const_name "op ="},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   67.53 +  | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   67.54      let
   67.55        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   67.56          val _ = map is_number [a,b,c]
    68.1 --- a/src/HOL/Tools/recfun_codegen.ML	Sat Aug 28 20:24:40 2010 +0800
    68.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Sat Aug 28 16:14:32 2010 +0200
    68.3 @@ -40,7 +40,7 @@
    68.4        end
    68.5    | avoid_value thy thms = thms;
    68.6  
    68.7 -fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
    68.8 +fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name HOL.eq} then ([], "") else
    68.9    let
   68.10      val c = AxClass.unoverload_const thy (raw_c, T);
   68.11      val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c
    69.1 --- a/src/HOL/Tools/record.ML	Sat Aug 28 20:24:40 2010 +0800
    69.2 +++ b/src/HOL/Tools/record.ML	Sat Aug 28 16:14:32 2010 +0200
    69.3 @@ -1342,7 +1342,7 @@
    69.4  val eq_simproc =
    69.5    Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
    69.6      (fn thy => fn _ => fn t =>
    69.7 -      (case t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ =>
    69.8 +      (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
    69.9          (case rec_id ~1 T of
   69.10            "" => NONE
   69.11          | name =>
   69.12 @@ -1405,12 +1405,12 @@
   69.13                  else raise TERM ("", [x]);
   69.14                val sel' = Const (sel, Tsel) $ Bound 0;
   69.15                val (l, r) = if lr then (sel', x') else (x', sel');
   69.16 -            in Const (@{const_name "op ="}, Teq) $ l $ r end
   69.17 +            in Const (@{const_name HOL.eq}, Teq) $ l $ r end
   69.18            else raise TERM ("", [Const (sel, Tsel)]);
   69.19  
   69.20 -        fun dest_sel_eq (Const (@{const_name "op ="}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
   69.21 +        fun dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
   69.22                (true, Teq, (sel, Tsel), X)
   69.23 -          | dest_sel_eq (Const (@{const_name "op ="}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
   69.24 +          | dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
   69.25                (false, Teq, (sel, Tsel), X)
   69.26            | dest_sel_eq _ = raise TERM ("", []);
   69.27        in
   69.28 @@ -1845,7 +1845,7 @@
   69.29      val eq =
   69.30        (HOLogic.mk_Trueprop o HOLogic.mk_eq)
   69.31          (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
   69.32 -         Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
   69.33 +         Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT));
   69.34      fun tac eq_def =
   69.35        Class.intro_classes_tac []
   69.36        THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def])
    70.1 --- a/src/HOL/Tools/refute.ML	Sat Aug 28 20:24:40 2010 +0800
    70.2 +++ b/src/HOL/Tools/refute.ML	Sat Aug 28 16:14:32 2010 +0200
    70.3 @@ -647,7 +647,7 @@
    70.4        | Const (@{const_name Hilbert_Choice.Eps}, _) => t
    70.5        | Const (@{const_name All}, _) => t
    70.6        | Const (@{const_name Ex}, _) => t
    70.7 -      | Const (@{const_name "op ="}, _) => t
    70.8 +      | Const (@{const_name HOL.eq}, _) => t
    70.9        | Const (@{const_name HOL.conj}, _) => t
   70.10        | Const (@{const_name HOL.disj}, _) => t
   70.11        | Const (@{const_name HOL.implies}, _) => t
   70.12 @@ -823,7 +823,7 @@
   70.13          end
   70.14        | Const (@{const_name All}, T) => collect_type_axioms T axs
   70.15        | Const (@{const_name Ex}, T) => collect_type_axioms T axs
   70.16 -      | Const (@{const_name "op ="}, T) => collect_type_axioms T axs
   70.17 +      | Const (@{const_name HOL.eq}, T) => collect_type_axioms T axs
   70.18        | Const (@{const_name HOL.conj}, _) => axs
   70.19        | Const (@{const_name HOL.disj}, _) => axs
   70.20        | Const (@{const_name HOL.implies}, _) => axs
   70.21 @@ -1850,16 +1850,16 @@
   70.22        end
   70.23      | Const (@{const_name Ex}, _) =>
   70.24        SOME (interpret thy model args (eta_expand t 1))
   70.25 -    | Const (@{const_name "op ="}, _) $ t1 $ t2 =>  (* similar to "==" (Pure) *)
   70.26 +    | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>  (* similar to "==" (Pure) *)
   70.27        let
   70.28          val (i1, m1, a1) = interpret thy model args t1
   70.29          val (i2, m2, a2) = interpret thy m1 a1 t2
   70.30        in
   70.31          SOME (make_equality (i1, i2), m2, a2)
   70.32        end
   70.33 -    | Const (@{const_name "op ="}, _) $ t1 =>
   70.34 +    | Const (@{const_name HOL.eq}, _) $ t1 =>
   70.35        SOME (interpret thy model args (eta_expand t 1))
   70.36 -    | Const (@{const_name "op ="}, _) =>
   70.37 +    | Const (@{const_name HOL.eq}, _) =>
   70.38        SOME (interpret thy model args (eta_expand t 2))
   70.39      | Const (@{const_name HOL.conj}, _) $ t1 $ t2 =>
   70.40        (* 3-valued logic *)
    71.1 --- a/src/HOL/Tools/simpdata.ML	Sat Aug 28 20:24:40 2010 +0800
    71.2 +++ b/src/HOL/Tools/simpdata.ML	Sat Aug 28 16:14:32 2010 +0200
    71.3 @@ -10,7 +10,7 @@
    71.4  structure Quantifier1 = Quantifier1Fun
    71.5  (struct
    71.6    (*abstract syntax*)
    71.7 -  fun dest_eq ((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME (c, s, t)
    71.8 +  fun dest_eq ((c as Const(@{const_name HOL.eq},_)) $ s $ t) = SOME (c, s, t)
    71.9      | dest_eq _ = NONE;
   71.10    fun dest_conj ((c as Const(@{const_name HOL.conj},_)) $ s $ t) = SOME (c, s, t)
   71.11      | dest_conj _ = NONE;
   71.12 @@ -44,7 +44,7 @@
   71.13  fun mk_eq th = case concl_of th
   71.14    (*expects Trueprop if not == *)
   71.15    of Const (@{const_name "=="},_) $ _ $ _ => th
   71.16 -   | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => mk_meta_eq th
   71.17 +   | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th
   71.18     | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
   71.19     | _ => th RS @{thm Eq_TrueI}
   71.20  
    72.1 --- a/src/HOL/ex/Meson_Test.thy	Sat Aug 28 20:24:40 2010 +0800
    72.2 +++ b/src/HOL/ex/Meson_Test.thy	Sat Aug 28 16:14:32 2010 +0200
    72.3 @@ -10,7 +10,7 @@
    72.4    below and constants declared in HOL!
    72.5  *}
    72.6  
    72.7 -hide_const (open) implies union inter subset sum quotient 
    72.8 +hide_const (open) eq implies union inter subset sum quotient 
    72.9  
   72.10  text {*
   72.11    Test data for the MESON proof procedure
    73.1 --- a/src/HOL/ex/SVC_Oracle.thy	Sat Aug 28 20:24:40 2010 +0800
    73.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Sat Aug 28 16:14:32 2010 +0200
    73.3 @@ -94,7 +94,7 @@
    73.4        | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
    73.5        | fm ((c as Const(@{const_name True}, _))) = c
    73.6        | fm ((c as Const(@{const_name False}, _))) = c
    73.7 -      | fm (t as Const(@{const_name "op ="},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    73.8 +      | fm (t as Const(@{const_name HOL.eq},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    73.9        | fm (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   73.10        | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   73.11        | fm t = replace t
    74.1 --- a/src/HOL/ex/svc_funcs.ML	Sat Aug 28 20:24:40 2010 +0800
    74.2 +++ b/src/HOL/ex/svc_funcs.ML	Sat Aug 28 16:14:32 2010 +0200
    74.3 @@ -95,7 +95,7 @@
    74.4             | Const(@{const_name Not}, _)    => apply c (map tag ts)
    74.5             | Const(@{const_name True}, _)   => (c, false)
    74.6             | Const(@{const_name False}, _)  => (c, false)
    74.7 -           | Const(@{const_name "op ="}, Type ("fun", [T,_])) =>
    74.8 +           | Const(@{const_name HOL.eq}, Type ("fun", [T,_])) =>
    74.9                   if T = HOLogic.boolT then
   74.10                       (*biconditional: with int/nat comparisons below?*)
   74.11                       let val [t1,t2] = ts
   74.12 @@ -200,7 +200,7 @@
   74.13              Buildin("AND",   (*unfolding uses both polarities*)
   74.14                           [Buildin("=>", [fm (not pos) p, fm pos q]),
   74.15                            Buildin("=>", [fm (not pos) q, fm pos p])])
   74.16 -      | fm pos (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ x $ y) =
   74.17 +      | fm pos (t as Const(@{const_name HOL.eq}, Type ("fun", [T,_])) $ x $ y) =
   74.18              let val tx = tm x and ty = tm y
   74.19                  in if pos orelse T = HOLogic.realT then
   74.20                         Buildin("=", [tx, ty])
    75.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML	Sat Aug 28 20:24:40 2010 +0800
    75.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML	Sat Aug 28 16:14:32 2010 +0200
    75.3 @@ -190,9 +190,9 @@
    75.4  
    75.5  fun mk_All  (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
    75.6  
    75.7 -infixr 0 ===>;  fun S ===> T = %%:"==>" $ S $ T;
    75.8 -infix 0 ==;     fun S ==  T = %%:"==" $ S $ T;
    75.9 -infix 1 ===;    fun S === T = %%:"op =" $ S $ T;
   75.10 +infixr 0 ===>;  fun S ===> T = %%: "==>" $ S $ T;
   75.11 +infix 0 ==;     fun S ==  T = %%: "==" $ S $ T;
   75.12 +infix 1 ===;    fun S === T = %%: @{const_name HOL.eq} $ S $ T;
   75.13  infix 1 ~=;     fun S ~=  T = HOLogic.mk_not (S === T);
   75.14  
   75.15  infix 9 `  ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x;