# HG changeset patch
# User haftmann
# Date 1142001228 -3600
# Node ID 77ca20b0ed7782849ce2f9d26b5219c14005808b
# Parent  1f5b5dc3f48a529218be9ab788261cc409ba3121
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.

diff -r 1f5b5dc3f48a -r 77ca20b0ed77 NEWS
--- a/NEWS	Fri Mar 10 12:28:38 2006 +0100
+++ b/NEWS	Fri Mar 10 15:33:48 2006 +0100
@@ -340,6 +340,33 @@
 25 like -->); output depends on the "iff" print_mode, the default is
 "A = B" (with priority 50).
 
+* Renamed some (legacy-named) constants in HOL.thy:
+    op +   ~> HOL.plus
+    op -   ~> HOL.minus
+    uminus ~> HOL.uminus
+    op *   ~> HOL.times
+
+Adaptions may be required in the following cases:
+
+a) User-defined constants using any of the names "plus", "minus", or "times"
+The standard syntax translations for "+", "-" and "*" may go wrong.
+INCOMPATIBILITY: use more specific names.
+
+b) Variables named "plus", "minus", or "times"
+INCOMPATIBILITY: use more specific names.
+
+c) Commutative equations theorems (e. g. "a + b = b + a")
+Since the changing of names also changes the order of terms, commutative rewrites
+perhaps will be applied when not applied before or the other way round.
+Experience shows that thiis is rarely the case (only two adaptions in the whole
+Isabelle distribution).
+INCOMPATIBILITY: rewrite proof; sometimes already an exchange of a distributive
+law may suffice.
+
+d) ML code directly refering to constant names
+This in general only affects hand-written proof tactics, simprocs and so on.
+INCOMPATIBILITY: grep your sourcecode and replace names.
+
 * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only).
 
 * In the context of the assumption "~(s = t)" the Simplifier rewrites
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Algebra/CRing.thy
--- a/src/HOL/Algebra/CRing.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Algebra/CRing.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -20,7 +20,7 @@
   a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
   "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
 
-  minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
+  a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
   "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y == x \<oplus> (\<ominus> y)"
 
 locale abelian_monoid = struct G +
@@ -95,7 +95,7 @@
 
 lemma (in abelian_group) minus_closed [intro, simp]:
   "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y \<in> carrier G"
-  by (simp add: minus_def)
+  by (simp add: a_minus_def)
 
 lemma (in abelian_group) a_l_cancel [simp]:
   "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
@@ -431,7 +431,7 @@
 
 lemma (in ring) minus_eq:
   "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
-  by (simp only: minus_def)
+  by (simp only: a_minus_def)
 
 lemmas (in ring) ring_simprules =
   a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Algebra/abstract/order.ML
--- a/src/HOL/Algebra/abstract/order.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Algebra/abstract/order.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -8,7 +8,7 @@
 (*** Term order for commutative rings ***)
 
 fun ring_ord a =
-  find_index_eq a ["0", "op +", "uminus", "op -", "1", "op *"];
+  find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus", "1", "HOL.times"];
 
 fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
 
@@ -18,9 +18,9 @@
 val a = Free ("a", intT);
 val b = Free ("b", intT);
 val c = Free ("c", intT);
-val plus = Const ("op +", [intT, intT]--->intT);
-val mult = Const ("op *", [intT, intT]--->intT);
-val uminus = Const ("uminus", intT-->intT);
+val plus = Const ("HOL.plus", [intT, intT]--->intT);
+val mult = Const ("HOL.times", [intT, intT]--->intT);
+val uminus = Const ("HOL.uminus", intT-->intT);
 val one = Const ("1", intT);
 val f = Const("f", intT-->intT);
 
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Auth/Guard/Extensions.thy
--- a/src/HOL/Auth/Guard/Extensions.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -27,15 +27,15 @@
 
 subsection{*Extensions to Theory @{text List}*}
 
-subsubsection{*"minus l x" erase the first element of "l" equal to "x"*}
+subsubsection{*"remove l x" erase the first element of "l" equal to "x"*}
 
-consts minus :: "'a list => 'a => 'a list"
+consts remove :: "'a list => 'a => 'a list"
 
 primrec
-"minus [] y = []"
-"minus (x#xs) y = (if x=y then xs else x # minus xs y)"
+"remove [] y = []"
+"remove (x#xs) y = (if x=y then xs else x # remove xs y)"
 
-lemma set_minus: "set (minus l x) <= set l"
+lemma set_remove: "set (remove l x) <= set l"
 by (induct l, auto)
 
 subsection{*Extensions to Theory @{text Message}*}
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Auth/Guard/Guard.thy
--- a/src/HOL/Auth/Guard/Guard.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Auth/Guard/Guard.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -208,7 +208,7 @@
 
 lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst]
 
-lemma cnb_minus [simp]: "x mem l ==> cnb (minus l x) = cnb l - crypt_nb x"
+lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x"
 apply (induct l, auto)
 by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
 
@@ -242,7 +242,7 @@
 subsection{*list corresponding to "decrypt"*}
 
 constdefs decrypt' :: "msg list => key => msg => msg list"
-"decrypt' l K Y == Y # minus l (Crypt K Y)"
+"decrypt' l K Y == Y # remove l (Crypt K Y)"
 
 declare decrypt'_def [simp]
 
@@ -278,7 +278,7 @@
 apply (subgoal_tac "Crypt K Y:parts (set l)")
 apply (drule parts_cnb, rotate_tac -1, simp)
 apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
-apply (rule insert_mono, rule set_minus)
+apply (rule insert_mono, rule set_remove)
 apply (simp add: analz_insertD, blast)
 (* Crypt K Y:parts (set l) *)
 apply (blast dest: kparts_parts)
@@ -288,7 +288,7 @@
 apply (rule_tac K=K in guard_Crypt, simp add: Guard_def, simp)
 apply (drule_tac t="set l'" in sym, simp)
 apply (rule Guard_kparts, simp, simp)
-apply (rule_tac B="set l'" in subset_trans, rule set_minus, blast)
+apply (rule_tac B="set l'" in subset_trans, rule set_remove, blast)
 by (rule kparts_set)
 
 lemma Guard_invKey_finite: "[| Nonce n:analz G; Guard n Ks G; finite G |]
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Auth/Guard/GuardK.thy
--- a/src/HOL/Auth/Guard/GuardK.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -204,7 +204,7 @@
 
 lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst]
 
-lemma cnb_minus [simp]: "x mem l ==> cnb (minus l x) = cnb l - crypt_nb x"
+lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x"
 apply (induct l, auto)
 by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
 
@@ -238,7 +238,7 @@
 subsection{*list corresponding to "decrypt"*}
 
 constdefs decrypt' :: "msg list => key => msg => msg list"
-"decrypt' l K Y == Y # minus l (Crypt K Y)"
+"decrypt' l K Y == Y # remove l (Crypt K Y)"
 
 declare decrypt'_def [simp]
 
@@ -274,7 +274,7 @@
 apply (subgoal_tac "Crypt K Y:parts (set l)")
 apply (drule parts_cnb, rotate_tac -1, simp)
 apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
-apply (rule insert_mono, rule set_minus)
+apply (rule insert_mono, rule set_remove)
 apply (simp add: analz_insertD, blast)
 (* Crypt K Y:parts (set l) *)
 apply (blast dest: kparts_parts)
@@ -284,7 +284,7 @@
 apply (rule_tac K=K in guardK_Crypt, simp add: GuardK_def, simp)
 apply (drule_tac t="set l'" in sym, simp)
 apply (rule GuardK_kparts, simp, simp)
-apply (rule_tac B="set l'" in subset_trans, rule set_minus, blast)
+apply (rule_tac B="set l'" in subset_trans, rule set_remove, blast)
 by (rule kparts_set)
 
 lemma GuardK_invKey_finite: "[| Key n:analz G; GuardK n Ks G; finite G |]
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Complex/CLim.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -976,7 +976,7 @@
 apply (simp add: diff_minus)
 apply (drule_tac f = g in CDERIV_inverse_fun)
 apply (drule_tac [2] CDERIV_mult, assumption+)
-apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left 
+apply (simp add: divide_inverse left_distrib power_inverse minus_mult_left 
                  mult_ac 
             del: minus_mult_right [symmetric] minus_mult_left [symmetric]
                  complexpow_Suc)
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/HOL.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -198,15 +198,20 @@
 axclass times < type
 axclass inverse < type
 
+consts
+  plus             :: "['a::plus, 'a]  => 'a"       (infixl "+" 65)
+  uminus           :: "'a::minus => 'a"             ("- _" [81] 80)
+  minus            :: "['a::minus, 'a] => 'a"       (infixl "-" 65)
+  abs              :: "'a::minus => 'a"
+  times            :: "['a::times, 'a] => 'a"       (infixl "*" 70)
+  inverse          :: "'a::inverse => 'a"
+  divide           :: "['a::inverse, 'a] => 'a"     (infixl "'/" 70)
+
 global
 
 consts
   "0"           :: "'a::zero"                       ("0")
   "1"           :: "'a::one"                        ("1")
-  "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
-  -             :: "['a::minus, 'a] => 'a"          (infixl 65)
-  uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
-  *             :: "['a::times, 'a] => 'a"          (infixl 70)
 
 syntax
   "_index1"  :: index    ("\<^sub>1")
@@ -223,12 +228,6 @@
   in [tr' "0", tr' "1"] end;
 *} -- {* show types that are presumably too general *}
 
-
-consts
-  abs           :: "'a::minus => 'a"
-  inverse       :: "'a::inverse => 'a"
-  divide        :: "['a::inverse, 'a] => 'a"        (infixl "'/" 70)
-
 syntax (xsymbols)
   abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
 syntax (HTML output)
@@ -1408,11 +1407,7 @@
   "op -->" "HOL.op_implies"
   "op &" "HOL.op_and"
   "op |" "HOL.op_or"
-  "op +" "HOL.op_add"
-  "op -" "HOL.op_minus"
-  "op *" "HOL.op_times"
   Not "HOL.not"
-  uminus "HOL.uminus"
   arbitrary "HOL.arbitrary"
 
 code_syntax_const
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -182,9 +182,9 @@
   ">="         > HOL4Compat.nat_ge
   FUNPOW       > HOL4Compat.FUNPOW
   "<="         > "op <="          :: "[nat,nat]=>bool"
-  "+"          > "op +"           :: "[nat,nat]=>nat"
-  "*"          > "op *"           :: "[nat,nat]=>nat"
-  "-"          > "op -"           :: "[nat,nat]=>nat"
+  "+"          > "HOL.plus"       :: "[nat,nat]=>nat"
+  "*"          > "HOL.times"      :: "[nat,nat]=>nat"
+  "-"          > "HOL.minus"      :: "[nat,nat]=>nat"
   MIN          > Orderings.min    :: "[nat,nat]=>nat"
   MAX          > Orderings.max    :: "[nat,nat]=>nat"
   DIV          > "Divides.op div" :: "[nat,nat]=>nat"
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Import/Generate-HOL/GenHOL4Real.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -21,8 +21,8 @@
   real_1   > 1           :: real
   real_neg > uminus      :: "real => real"
   inv      > HOL.inverse :: "real => real"
-  real_add > "op +"      :: "[real,real] => real"
-  real_mul > "op *"      :: "[real,real] => real"
+  real_add > HOL.plus    :: "[real,real] => real"
+  real_mul > HOL.times   :: "[real,real] => real"
   real_lt  > "op <"      :: "[real,real] => bool";
 
 ignore_thms
@@ -52,7 +52,7 @@
   real_gt     > HOL4Compat.real_gt
   real_ge     > HOL4Compat.real_ge
   real_lte    > "op <="      :: "[real,real] => bool"
-  real_sub    > "op -"       :: "[real,real] => real"
+  real_sub    > HOL.minus    :: "[real,real] => real"
   "/"         > HOL.divide   :: "[real,real] => real"
   pow         > Nat.power    :: "[real,nat] => real"
   abs         > HOL.abs      :: "real => real"
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -76,9 +76,9 @@
   SUC > Suc
   PRE > HOLLightCompat.Pred
   NUMERAL > HOL4Compat.NUMERAL
-  "+" > "op +" :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
-  "*" > "op *" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  "-" > "op -" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  "+" > HOL.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
+  "*" > HOL.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  "-" > HOL.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   BIT0 > HOLLightCompat.NUMERAL_BIT0
   BIT1 > HOL4Compat.NUMERAL_BIT1
   INL > Sum_Type.Inl
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Import/HOL/arithmetic.imp
--- a/src/HOL/Import/HOL/arithmetic.imp	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Import/HOL/arithmetic.imp	Fri Mar 10 15:33:48 2006 +0100
@@ -24,9 +24,9 @@
   ">=" > "HOL4Compat.nat_ge"
   ">" > "HOL4Compat.nat_gt"
   "<=" > "op <=" :: "nat => nat => bool"
-  "-" > "op -" :: "nat => nat => nat"
-  "+" > "op +" :: "nat => nat => nat"
-  "*" > "op *" :: "nat => nat => nat"
+  "-" > "HOL.minus" :: "nat => nat => nat"
+  "+" > "HOL.plus" :: "nat => nat => nat"
+  "*" > "HOL.times" :: "nat => nat => nat"
 
 thm_maps
   "num_case_def" > "HOL4Compat.num_case_def"
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Import/HOL/real.imp
--- a/src/HOL/Import/HOL/real.imp	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Import/HOL/real.imp	Fri Mar 10 15:33:48 2006 +0100
@@ -10,7 +10,7 @@
 const_maps
   "sup" > "HOL4Real.real.sup"
   "sum" > "HOL4Real.real.sum"
-  "real_sub" > "op -" :: "real => real => real"
+  "real_sub" > "HOL.minus" :: "real => real => real"
   "real_of_num" > "RealDef.real" :: "nat => real"
   "real_lte" > "op <=" :: "real => real => bool"
   "real_gt" > "HOL4Compat.real_gt"
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Import/HOL/realax.imp
--- a/src/HOL/Import/HOL/realax.imp	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Import/HOL/realax.imp	Fri Mar 10 15:33:48 2006 +0100
@@ -27,10 +27,10 @@
   "treal_add" > "HOL4Real.realax.treal_add"
   "treal_1" > "HOL4Real.realax.treal_1"
   "treal_0" > "HOL4Real.realax.treal_0"
-  "real_neg" > "uminus" :: "real => real"
-  "real_mul" > "op *" :: "real => real => real"
+  "real_neg" > "HOL.uminus" :: "real => real"
+  "real_mul" > "HOL.times" :: "real => real => real"
   "real_lt" > "op <" :: "real => real => bool"
-  "real_add" > "op +" :: "real => real => real"
+  "real_add" > "HOL.plus" :: "real => real => real"
   "real_1" > "1" :: "real"
   "real_0" > "0" :: "real"
   "inv" > "HOL.inverse" :: "real => real"
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Import/HOLLight/HOLLight.thy
--- a/src/HOL/Import/HOLLight/HOLLight.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Import/HOLLight/HOLLight.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -1119,37 +1119,37 @@
    (%x::nat.
        (All::(nat => bool) => bool)
         (%xa::nat.
-            (op =::nat => nat => bool) ((op +::nat => nat => nat) x xa)
-             ((op +::nat => nat => nat) x xa))))
+            (op =::nat => nat => bool) ((HOL.plus::nat => nat => nat) x xa)
+             ((HOL.plus::nat => nat => nat) x xa))))
  ((op &::bool => bool => bool)
-   ((op =::nat => nat => bool) ((op +::nat => nat => nat) (0::nat) (0::nat))
+   ((op =::nat => nat => bool) ((HOL.plus::nat => nat => nat) (0::nat) (0::nat))
      (0::nat))
    ((op &::bool => bool => bool)
      ((All::(nat => bool) => bool)
        (%x::nat.
            (op =::nat => nat => bool)
-            ((op +::nat => nat => nat) (0::nat)
+            ((HOL.plus::nat => nat => nat) (0::nat)
               ((NUMERAL_BIT0::nat => nat) x))
             ((NUMERAL_BIT0::nat => nat) x)))
      ((op &::bool => bool => bool)
        ((All::(nat => bool) => bool)
          (%x::nat.
              (op =::nat => nat => bool)
-              ((op +::nat => nat => nat) (0::nat)
+              ((HOL.plus::nat => nat => nat) (0::nat)
                 ((NUMERAL_BIT1::nat => nat) x))
               ((NUMERAL_BIT1::nat => nat) x)))
        ((op &::bool => bool => bool)
          ((All::(nat => bool) => bool)
            (%x::nat.
                (op =::nat => nat => bool)
-                ((op +::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
+                ((HOL.plus::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
                   (0::nat))
                 ((NUMERAL_BIT0::nat => nat) x)))
          ((op &::bool => bool => bool)
            ((All::(nat => bool) => bool)
              (%x::nat.
                  (op =::nat => nat => bool)
-                  ((op +::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
+                  ((HOL.plus::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
                     (0::nat))
                   ((NUMERAL_BIT1::nat => nat) x)))
            ((op &::bool => bool => bool)
@@ -1158,44 +1158,44 @@
                    (All::(nat => bool) => bool)
                     (%xa::nat.
                         (op =::nat => nat => bool)
-                         ((op +::nat => nat => nat)
+                         ((HOL.plus::nat => nat => nat)
                            ((NUMERAL_BIT0::nat => nat) x)
                            ((NUMERAL_BIT0::nat => nat) xa))
                          ((NUMERAL_BIT0::nat => nat)
-                           ((op +::nat => nat => nat) x xa)))))
+                           ((HOL.plus::nat => nat => nat) x xa)))))
              ((op &::bool => bool => bool)
                ((All::(nat => bool) => bool)
                  (%x::nat.
                      (All::(nat => bool) => bool)
                       (%xa::nat.
                           (op =::nat => nat => bool)
-                           ((op +::nat => nat => nat)
+                           ((HOL.plus::nat => nat => nat)
                              ((NUMERAL_BIT0::nat => nat) x)
                              ((NUMERAL_BIT1::nat => nat) xa))
                            ((NUMERAL_BIT1::nat => nat)
-                             ((op +::nat => nat => nat) x xa)))))
+                             ((HOL.plus::nat => nat => nat) x xa)))))
                ((op &::bool => bool => bool)
                  ((All::(nat => bool) => bool)
                    (%x::nat.
                        (All::(nat => bool) => bool)
                         (%xa::nat.
                             (op =::nat => nat => bool)
-                             ((op +::nat => nat => nat)
+                             ((HOL.plus::nat => nat => nat)
                                ((NUMERAL_BIT1::nat => nat) x)
                                ((NUMERAL_BIT0::nat => nat) xa))
                              ((NUMERAL_BIT1::nat => nat)
-                               ((op +::nat => nat => nat) x xa)))))
+                               ((HOL.plus::nat => nat => nat) x xa)))))
                  ((All::(nat => bool) => bool)
                    (%x::nat.
                        (All::(nat => bool) => bool)
                         (%xa::nat.
                             (op =::nat => nat => bool)
-                             ((op +::nat => nat => nat)
+                             ((HOL.plus::nat => nat => nat)
                                ((NUMERAL_BIT1::nat => nat) x)
                                ((NUMERAL_BIT1::nat => nat) xa))
                              ((NUMERAL_BIT0::nat => nat)
                                ((Suc::nat => nat)
-                                 ((op +::nat => nat => nat) x
+                                 ((HOL.plus::nat => nat => nat) x
                                    xa))))))))))))))"
   by (import hollight ARITH_ADD)
 
@@ -1258,7 +1258,7 @@
                            ((op *::nat => nat => nat)
                              ((NUMERAL_BIT0::nat => nat) x)
                              ((NUMERAL_BIT1::nat => nat) xa))
-                           ((op +::nat => nat => nat)
+                           ((HOL.plus::nat => nat => nat)
                              ((NUMERAL_BIT0::nat => nat) x)
                              ((NUMERAL_BIT0::nat => nat)
                                ((NUMERAL_BIT0::nat => nat)
@@ -1272,7 +1272,7 @@
                              ((op *::nat => nat => nat)
                                ((NUMERAL_BIT1::nat => nat) x)
                                ((NUMERAL_BIT0::nat => nat) xa))
-                             ((op +::nat => nat => nat)
+                             ((HOL.plus::nat => nat => nat)
                                ((NUMERAL_BIT0::nat => nat) xa)
                                ((NUMERAL_BIT0::nat => nat)
                                  ((NUMERAL_BIT0::nat => nat)
@@ -1285,9 +1285,9 @@
                              ((op *::nat => nat => nat)
                                ((NUMERAL_BIT1::nat => nat) x)
                                ((NUMERAL_BIT1::nat => nat) xa))
-                             ((op +::nat => nat => nat)
+                             ((HOL.plus::nat => nat => nat)
                                ((NUMERAL_BIT1::nat => nat) x)
-                               ((op +::nat => nat => nat)
+                               ((HOL.plus::nat => nat => nat)
                                  ((NUMERAL_BIT0::nat => nat) xa)
                                  ((NUMERAL_BIT0::nat => nat)
                                    ((NUMERAL_BIT0::nat => nat)
@@ -7462,7 +7462,7 @@
       (%i::nat.
           ($::('A::type, ('M::type, 'N::type) finite_sum) cart
               => nat => 'A::type)
-           u ((op +::nat => nat => nat) i
+           u ((HOL.plus::nat => nat => nat) i
                ((dimindex::('M::type => bool) => nat)
                  (hollight.UNIV::'M::type => bool)))))"
 
@@ -7478,14 +7478,14 @@
       (%i::nat.
           ($::('A::type, ('M::type, 'N::type) finite_sum) cart
               => nat => 'A::type)
-           u ((op +::nat => nat => nat) i
+           u ((HOL.plus::nat => nat => nat) i
                ((dimindex::('M::type => bool) => nat)
                  (hollight.UNIV::'M::type => bool)))))"
   by (import hollight DEF_sndcart)
 
 lemma DIMINDEX_HAS_SIZE_FINITE_SUM: "(HAS_SIZE::(('M::type, 'N::type) finite_sum => bool) => nat => bool)
  (hollight.UNIV::('M::type, 'N::type) finite_sum => bool)
- ((op +::nat => nat => nat)
+ ((HOL.plus::nat => nat => nat)
    ((dimindex::('M::type => bool) => nat) (hollight.UNIV::'M::type => bool))
    ((dimindex::('N::type => bool) => nat)
      (hollight.UNIV::'N::type => bool)))"
@@ -7494,7 +7494,7 @@
 lemma DIMINDEX_FINITE_SUM: "(op =::nat => nat => bool)
  ((dimindex::(('M::type, 'N::type) finite_sum => bool) => nat)
    (hollight.UNIV::('M::type, 'N::type) finite_sum => bool))
- ((op +::nat => nat => nat)
+ ((HOL.plus::nat => nat => nat)
    ((dimindex::('M::type => bool) => nat) (hollight.UNIV::'M::type => bool))
    ((dimindex::('N::type => bool) => nat)
      (hollight.UNIV::'N::type => bool)))"
@@ -8025,7 +8025,7 @@
  (nsum::('q_51017::type => bool) => ('q_51017::type => nat) => nat)
  ((iterate::(nat => nat => nat)
             => ('q_51017::type => bool) => ('q_51017::type => nat) => nat)
-   (op +::nat => nat => nat))"
+   (HOL.plus::nat => nat => nat))"
 
 lemma DEF_nsum: "(op =::(('q_51017::type => bool) => ('q_51017::type => nat) => nat)
        => (('q_51017::type => bool) => ('q_51017::type => nat) => nat)
@@ -8033,17 +8033,17 @@
  (nsum::('q_51017::type => bool) => ('q_51017::type => nat) => nat)
  ((iterate::(nat => nat => nat)
             => ('q_51017::type => bool) => ('q_51017::type => nat) => nat)
-   (op +::nat => nat => nat))"
+   (HOL.plus::nat => nat => nat))"
   by (import hollight DEF_nsum)
 
 lemma NEUTRAL_ADD: "(op =::nat => nat => bool)
- ((neutral::(nat => nat => nat) => nat) (op +::nat => nat => nat)) (0::nat)"
+ ((neutral::(nat => nat => nat) => nat) (HOL.plus::nat => nat => nat)) (0::nat)"
   by (import hollight NEUTRAL_ADD)
 
 lemma NEUTRAL_MUL: "neutral op * = NUMERAL_BIT1 0"
   by (import hollight NEUTRAL_MUL)
 
-lemma MONOIDAL_ADD: "(monoidal::(nat => nat => nat) => bool) (op +::nat => nat => nat)"
+lemma MONOIDAL_ADD: "(monoidal::(nat => nat => nat) => bool) (HOL.plus::nat => nat => nat)"
   by (import hollight MONOIDAL_ADD)
 
 lemma MONOIDAL_MUL: "(monoidal::(nat => nat => nat) => bool) (op *::nat => nat => nat)"
@@ -8068,7 +8068,7 @@
   by (import hollight NSUM_DIFF)
 
 lemma NSUM_SUPPORT: "ALL (x::'q_51214::type => nat) xa::'q_51214::type => bool.
-   FINITE (support op + x xa) --> nsum (support op + x xa) x = nsum xa x"
+   FINITE (support HOL.plus x xa) --> nsum (support HOL.plus x xa) x = nsum xa x"
   by (import hollight NSUM_SUPPORT)
 
 lemma NSUM_ADD: "ALL (f::'q_51260::type => nat) (g::'q_51260::type => nat)
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Import/HOLLight/hollight.imp
--- a/src/HOL/Import/HOLLight/hollight.imp	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Import/HOLLight/hollight.imp	Fri Mar 10 15:33:48 2006 +0100
@@ -238,10 +238,10 @@
   "<=" > "HOLLight.hollight.<="
   "<" > "HOLLight.hollight.<"
   "/\\" > "op &"
-  "-" > "op -" :: "nat => nat => nat"
+  "-" > "HOL.minus" :: "nat => nat => nat"
   "," > "Pair"
-  "+" > "op +" :: "nat => nat => nat"
-  "*" > "op *" :: "nat => nat => nat"
+  "+" > "HOL.plus" :: "nat => nat => nat"
+  "*" > "HOL.times" :: "nat => nat => nat"
   "$" > "HOLLight.hollight.$"
   "!" > "All"
 
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -886,14 +886,14 @@
   by (simp add: nat_aux_def)
 
 consts_code
-  "0" :: "int"                  ("0")
-  "1" :: "int"                  ("1")
-  "uminus" :: "int => int"      ("~")
-  "op +" :: "int => int => int" ("(_ +/ _)")
-  "op *" :: "int => int => int" ("(_ */ _)")
-  "op <" :: "int => int => bool" ("(_ </ _)")
-  "op <=" :: "int => int => bool" ("(_ <=/ _)")
-  "neg"                         ("(_ < 0)")
+  "0" :: "int"                       ("0")
+  "1" :: "int"                       ("1")
+  "HOL.uminus" :: "int => int"       ("~")
+  "HOL.plus" :: "int => int => int"  ("(_ +/ _)")
+  "HOL.times" :: "int => int => int" ("(_ */ _)")
+  "op <" :: "int => int => bool"     ("(_ </ _)")
+  "op <=" :: "int => int => bool"    ("(_ <=/ _)")
+  "neg"                              ("(_ < 0)")
 
 code_syntax_tyco int
   ml (target_atom "IntInf.int")
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Integ/cooper_dec.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -116,8 +116,8 @@
  
 fun linear_cmul n tm =  if n = 0 then zero else let fun times n k = n*k in  
   ( case tm of  
-     (Const("op +",T)  $  (Const ("op *",T1 ) $c1 $  x1) $ rest) => 
-       Const("op +",T) $ ((Const("op *",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest) 
+     (Const("HOL.plus",T)  $  (Const ("HOL.times",T1 ) $c1 $  x1) $ rest) => 
+       Const("HOL.plus",T) $ ((Const("HOL.times",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest) 
     |_ =>  numeral1 (times n) tm) 
     end ; 
  
@@ -139,23 +139,23 @@
 fun linear_add vars tm1 tm2 = 
   let fun addwith x y = x + y in
  (case (tm1,tm2) of 
-	((Const ("op +",T1) $ ( Const("op *",T2) $ c1 $  x1) $ rest1),(Const 
-	("op +",T3)$( Const("op *",T4) $ c2 $  x2) $ rest2)) => 
+	((Const ("HOL.plus",T1) $ ( Const("HOL.times",T2) $ c1 $  x1) $ rest1),(Const 
+	("HOL.plus",T3)$( Const("HOL.times",T4) $ c2 $  x2) $ rest2)) => 
          if x1 = x2 then 
               let val c = (numeral2 (addwith) c1 c2) 
 	      in 
               if c = zero then (linear_add vars rest1  rest2)  
-	      else (Const("op +",T1) $ (Const("op *",T2) $ c $ x1) $ (linear_add vars  rest1 rest2)) 
+	      else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c $ x1) $ (linear_add vars  rest1 rest2)) 
               end 
 	   else 
-		if earlierv vars x1 x2 then (Const("op +",T1) $  
-		(Const("op *",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2)) 
-    	       else (Const("op +",T1) $ (Const("op *",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2)) 
-   	|((Const("op +",T1) $ (Const("op *",T2) $ c1 $ x1) $ rest1) ,_) => 
-    	  (Const("op +",T1)$ (Const("op *",T2) $ c1 $ x1) $ (linear_add vars 
+		if earlierv vars x1 x2 then (Const("HOL.plus",T1) $  
+		(Const("HOL.times",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2)) 
+    	       else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2)) 
+   	|((Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c1 $ x1) $ rest1) ,_) => 
+    	  (Const("HOL.plus",T1)$ (Const("HOL.times",T2) $ c1 $ x1) $ (linear_add vars 
 	  rest1 tm2)) 
-   	|(_, (Const("op +",T1) $(Const("op *",T2) $ c2 $ x2) $ rest2)) => 
-      	  (Const("op +",T1) $ (Const("op *",T2) $ c2 $ x2) $ (linear_add vars tm1 
+   	|(_, (Const("HOL.plus",T1) $(Const("HOL.times",T2) $ c2 $ x2) $ rest2)) => 
+      	  (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 
 	  rest2)) 
    	| (_,_) => numeral2 (addwith) tm1 tm2) 
 	 
@@ -180,13 +180,13 @@
  Free(x,T)*) 
   
 fun lint vars tm = if is_numeral tm then tm else case tm of 
-   (Free (x,T)) =>  (HOLogic.mk_binop "op +" ((HOLogic.mk_binop "op *" ((mk_numeral 1),Free (x,T))), zero)) 
-  |(Bound i) =>  (Const("op +",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ 
-  (Const("op *",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero) 
-  |(Const("uminus",_) $ t ) => (linear_neg (lint vars t)) 
-  |(Const("op +",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) 
-  |(Const("op -",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) 
-  |(Const ("op *",_) $ s $ t) => 
+   (Free (x,T)) =>  (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1),Free (x,T))), zero)) 
+  |(Bound i) =>  (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ 
+  (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero) 
+  |(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t)) 
+  |(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) 
+  |(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) 
+  |(Const ("HOL.times",_) $ s $ t) => 
         let val s' = lint vars s  
             val t' = lint vars t  
         in 
@@ -212,14 +212,14 @@
       end 
     else (warning "Nonlinear term --- Non numeral leftside at dvd"
       ;raise COOPER)
-  |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
-  |linform vars  (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
-  |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 
+  |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
+  |linform vars  (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
+  |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 
   |linform vars  (Const("op <=",_)$ s $ t ) = 
-        (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("op +",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s)) 
+        (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s)) 
   |linform vars  (Const("op >=",_)$ s $ t ) = 
-        (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> 
-	HOLogic.intT) $ (Const("op +",HOLogic.intT --> HOLogic.intT --> 
+        (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> 
+	HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> 
 	HOLogic.intT) $s $(mk_numeral 1)) $ t)) 
  
    |linform vars  fm =  fm; 
@@ -246,7 +246,7 @@
 fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); 
  
 fun formlcm x fm = case fm of 
-    (Const (p,_)$ _ $(Const ("op +", _)$(Const ("op *",_)$ c $ y ) $z ) ) =>  if 
+    (Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) =>  if 
     (is_arith_rel fm) andalso (x = y) then  (abs(dest_numeral c)) else 1 
   | ( Const ("Not", _) $p) => formlcm x p 
   | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) 
@@ -259,13 +259,13 @@
  
 fun adjustcoeff x l fm = 
      case fm of  
-      (Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $ 
+      (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
       c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
         let val m = l div (dest_numeral c) 
             val n = (if p = "op <" then abs(m) else m) 
-            val xtm = HOLogic.mk_binop "op *" ((mk_numeral (m div n)), x) 
+            val xtm = HOLogic.mk_binop "HOL.times" ((mk_numeral (m div n)), x) 
 	in
-        (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
+        (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
 	end 
 	else fm 
   |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeff x l p) 
@@ -282,8 +282,8 @@
       val fm' = adjustcoeff x l fm in
       if l = 1 then fm' 
 	 else 
-     let val xp = (HOLogic.mk_binop "op +"  
-     		((HOLogic.mk_binop "op *" ((mk_numeral 1), x )), zero))
+     let val xp = (HOLogic.mk_binop "HOL.plus"  
+     		((HOLogic.mk_binop "HOL.times" ((mk_numeral 1), x )), zero))
 	in 
       HOLogic.conj $(HOLogic.mk_binrel "Divides.op dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm) 
       end 
@@ -294,12 +294,12 @@
 (*
 fun adjustcoeffeq x l fm = 
     case fm of  
-      (Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $ 
+      (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
       c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
         let val m = l div (dest_numeral c) 
             val n = (if p = "op <" then abs(m) else m)  
-            val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
-            in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
+            val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
+            in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
 	    end 
 	else fm 
   |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeffeq x l p) 
@@ -315,11 +315,11 @@
 (* ------------------------------------------------------------------------- *) 
  
 fun minusinf x fm = case fm of  
-    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) => 
+    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) => 
   	 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const  
 	 				 else fm 
  
-  |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z 
+  |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z 
   )) => if (x = y) 
 	then if (pm1 = one) andalso (c = zero) then HOLogic.false_const 
 	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
@@ -336,11 +336,11 @@
 (* ------------------------------------------------------------------------- *)
 
 fun plusinf x fm = case fm of
-    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
+    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
   	 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
 	 				 else fm
 
-  |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z
+  |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
   )) => if (x = y) 
 	then if (pm1 = one) andalso (c = zero) then HOLogic.true_const 
 	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
@@ -356,7 +356,7 @@
 (* The LCM of all the divisors that involve x.                               *) 
 (* ------------------------------------------------------------------------- *) 
  
-fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z ) ) =  
+fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =  
         if x = y then abs(dest_numeral d) else 1 
   |divlcm x ( Const ("Not", _) $ p) = divlcm x p 
   |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q) 
@@ -370,15 +370,15 @@
 fun bset x fm = case fm of 
    (Const ("Not", _) $ p) => if (is_arith_rel p) then  
           (case p of  
-	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $c2 $y) $a ) )  
+	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )  
 	             => if (is_arith_rel p) andalso (x=	y) andalso (c2 = one) andalso (c1 = zero)  
 	                then [linear_neg a] 
 			else  bset x p 
    	  |_ =>[]) 
 			 
 			else bset x p 
-  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +",_) $ (Const ("op *",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))]  else [] 
-  |(Const ("op <",_) $ c1$ (Const ("op +",_) $(Const ("op *",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] 
+  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))]  else [] 
+  |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] 
   |(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q) 
   |(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q) 
   |_ => []; 
@@ -390,15 +390,15 @@
 fun aset x fm = case fm of
    (Const ("Not", _) $ p) => if (is_arith_rel p) then
           (case p of
-	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $c2 $y) $a ) )
+	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )
 	             => if (x=	y) andalso (c2 = one) andalso (c1 = zero)
 	                then [linear_neg a]
 			else  []
    	  |_ =>[])
 
 			else aset x p
-  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +",_) $ (Const ("op *",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a]  else []
-  |(Const ("op <",_) $ c1$ (Const ("op +",_) $(Const ("op *",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
+  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a]  else []
+  |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
   |(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
   |(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
   |_ => [];
@@ -409,7 +409,7 @@
 (* ------------------------------------------------------------------------- *) 
  
 fun linrep vars x t fm = case fm of  
-   ((Const(p,_)$ d $ (Const("op +",_)$(Const("op *",_)$ c $ y) $ z))) => 
+   ((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) => 
       if (x = y) andalso (is_arith_rel fm)  
       then  
         let val ct = linear_cmul (dest_numeral c) t  
@@ -435,8 +435,8 @@
    val dn = dest_numeral d
    fun coeffs_of x = case x of 
      Const(p,_) $ tl $ tr => 
-       if p = "op +" then (coeffs_of tl) union (coeffs_of tr)
-          else if p = "op *" 
+       if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr)
+          else if p = "HOL.times" 
 	        then if (is_numeral tr) 
 		 then [(dest_numeral tr) * (dest_numeral tl)] 
 		 else [dest_numeral tl]
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Integ/cooper_proof.ML
--- a/src/HOL/Integ/cooper_proof.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Integ/cooper_proof.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -165,11 +165,11 @@
 (* ------------------------------------------------------------------------- *)
 
 fun norm_zero_one fm = case fm of
-  (Const ("op *",_) $ c $ t) => 
+  (Const ("HOL.times",_) $ c $ t) => 
     if c = one then (norm_zero_one t)
     else if (dest_numeral c = ~1) 
-         then (Const("uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
-         else (HOLogic.mk_binop "op *" (norm_zero_one c,norm_zero_one t))
+         then (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
+         else (HOLogic.mk_binop "HOL.times" (norm_zero_one c,norm_zero_one t))
   |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
   |(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
   |_ => fm;
@@ -255,13 +255,13 @@
 (*==================================================*)
 
 fun decomp_adjustcoeffeq sg x l fm = case fm of
-    (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("op +", _)$(Const ("op *",_) $    c $ y ) $z )))) => 
+    (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $    c $ y ) $z )))) => 
      let  
         val m = l div (dest_numeral c) 
         val n = if (x = y) then abs (m) else 1
-        val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x)) 
+        val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x)) 
         val rs = if (x = y) 
-                 then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
+                 then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
                  else HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )
         val ck = cterm_of sg (mk_numeral n)
         val cc = cterm_of sg c
@@ -273,14 +273,14 @@
         in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
         end
 
-  |(Const(p,_) $a $( Const ("op +", _)$(Const ("op *",_) $ 
+  |(Const(p,_) $a $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
       c $ y ) $t )) => 
    if (is_arith_rel fm) andalso (x = y) 
    then  
         let val m = l div (dest_numeral c) 
            val k = (if p = "op <" then abs(m) else m)  
-           val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div k)*l) ), x))
-           val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul k t) )))) 
+           val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div k)*l) ), x))
+           val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) )))) 
 
            val ck = cterm_of sg (mk_numeral k)
            val cc = cterm_of sg c
@@ -335,28 +335,28 @@
    val cfalse = cterm_of sg HOLogic.false_const
    val fm = norm_zero_one fm1
   in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
+      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
          if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
            else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
 
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
+      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
   	   if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one) 
 	   then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf))
 	 	 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) 
 
-      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
+      |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
            if (y=x) andalso (c1 = zero) then 
             if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else
 	     (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
   
-      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
 			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
-      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
+      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
       c $ y ) $ z))) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
 			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
@@ -373,22 +373,22 @@
    let
    val fm = norm_zero_one fm1
     in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
+      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
          if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	   then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
            else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
 
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
+      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
   	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
 	     then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
 	     else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) 
 
-      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
+      |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
            if (y=x) andalso (c1 =zero) then 
             if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
 	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
-      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_minf)) 
@@ -396,7 +396,7 @@
 
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
 		
-      |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+      |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf))
@@ -431,30 +431,30 @@
   val cfalse = cterm_of sg HOLogic.false_const
   val fm = norm_zero_one fm1
  in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
+      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
          if ((x=y) andalso (c1= zero) andalso (c2= one))
 	 then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
          else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
 
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
+      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
   	if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero)  andalso (c2 = one)) 
 	then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
 	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
 
-      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
+      |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
         if ((y=x) andalso (c1 = zero)) then 
           if (pm1 = one) 
 	  then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf)) 
 	  else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
 	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
   
-      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
 			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
-      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
+      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
       c $ y ) $ z))) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
 			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
@@ -472,22 +472,22 @@
   let
 					val fm = norm_zero_one fm1
     in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
+      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
          if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	   then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
            else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
 
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
+      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
   	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
 	     then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
 	     else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) 
 
-      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
+      |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
            if (y=x) andalso (c1 =zero) then 
             if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
 	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
-      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_pinf)) 
@@ -495,7 +495,7 @@
 
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
 		
-      |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+      |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf))
@@ -567,31 +567,31 @@
     val cat = cterm_of sg (norm_zero_one at)
   in
   case at of 
-   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
+   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
       if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
-	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
+	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
 		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
 	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
 	 end
          else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
+   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
      if (is_arith_rel at) andalso (x=y)
 	then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
 	         in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
-	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("op -",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
+	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
 		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
 	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
 	 end
        end
          else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
+   |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
         if (y=x) andalso (c1 =zero) then 
         if pm1 = one then 
 	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
-              val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
+              val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
 	  in  (instantiate' [] [SOME cfma,  SOME cdlcm]([th1,th2] MRS (not_bst_p_gt)))
 	    end
 	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
@@ -599,7 +599,7 @@
 	      end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
       if y=x then  
            let val cz = cterm_of sg (norm_zero_one z)
 	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
@@ -607,7 +607,7 @@
 	     end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+   |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
        if y=x then  
 	 let val cz = cterm_of sg (norm_zero_one z)
 	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
@@ -658,26 +658,26 @@
     val cat = cterm_of sg (norm_zero_one at)
   in
   case at of 
-   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
+   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
       if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A)
-	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
+	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
 		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
 	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
 	 end
          else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
+   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
      if (is_arith_rel at) andalso (x=y)
 	then let val ast_z = norm_zero_one (linear_sub [] one z )
 	         val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
-	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("op +",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
+	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("HOL.plus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
 		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
 	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
        end
          else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
+   |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
         if (y=x) andalso (c1 =zero) then 
         if pm1 = (mk_numeral ~1) then 
 	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
@@ -689,7 +689,7 @@
 	      end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
       if y=x then  
            let val cz = cterm_of sg (norm_zero_one z)
 	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
@@ -697,7 +697,7 @@
 	     end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+   |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
        if y=x then  
 	 let val cz = cterm_of sg (norm_zero_one z)
 	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Integ/int_arith1.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -197,11 +197,11 @@
          handle TERM _ => find_first_numeral (t::past) terms)
   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
 
-val mk_plus = HOLogic.mk_binop "op +";
+val mk_plus = HOLogic.mk_binop "HOL.plus";
 
 fun mk_minus t = 
   let val T = Term.fastype_of t
-  in Const ("uminus", T --> T) $ t
+  in Const ("HOL.uminus", T --> T) $ t
   end;
 
 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
@@ -213,22 +213,22 @@
 fun long_mk_sum T []        = mk_numeral T 0
   | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
 
-val dest_plus = HOLogic.dest_bin "op +" Term.dummyT;
+val dest_plus = HOLogic.dest_bin "HOL.plus" Term.dummyT;
 
 (*decompose additions AND subtractions as a sum*)
-fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) =
+fun dest_summing (pos, Const ("HOL.plus", _) $ t $ u, ts) =
         dest_summing (pos, t, dest_summing (pos, u, ts))
-  | dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
+  | dest_summing (pos, Const ("HOL.minus", _) $ t $ u, ts) =
         dest_summing (pos, t, dest_summing (not pos, u, ts))
   | dest_summing (pos, t, ts) =
         if pos then t::ts else mk_minus t :: ts;
 
 fun dest_sum t = dest_summing (true, t, []);
 
-val mk_diff = HOLogic.mk_binop "op -";
-val dest_diff = HOLogic.dest_bin "op -" Term.dummyT;
+val mk_diff = HOLogic.mk_binop "HOL.minus";
+val dest_diff = HOLogic.dest_bin "HOL.minus" Term.dummyT;
 
-val mk_times = HOLogic.mk_binop "op *";
+val mk_times = HOLogic.mk_binop "HOL.times";
 
 fun mk_prod T = 
   let val one = mk_numeral T 1
@@ -241,7 +241,7 @@
 fun long_mk_prod T []        = mk_numeral T 1
   | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
 
-val dest_times = HOLogic.dest_bin "op *" Term.dummyT;
+val dest_times = HOLogic.dest_bin "HOL.times" Term.dummyT;
 
 fun dest_prod t =
       let val (t,u) = dest_times t
@@ -252,7 +252,7 @@
 fun mk_coeff (k, t) = mk_times (mk_numeral (Term.fastype_of t) k, t);
 
 (*Express t as a product of (possibly) a numeral with other sorted terms*)
-fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
+fun dest_coeff sign (Const ("HOL.uminus", _) $ t) = dest_coeff (~sign) t
   | dest_coeff sign t =
     let val ts = sort Term.term_ord (dest_prod t)
         val (n, ts') = find_first_numeral [] ts
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -39,7 +39,7 @@
   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
 
 val zero = mk_numeral 0;
-val mk_plus = HOLogic.mk_binop "op +";
+val mk_plus = HOLogic.mk_binop "HOL.plus";
 
 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
 fun mk_sum []        = zero
@@ -50,7 +50,7 @@
 fun long_mk_sum []        = HOLogic.zero
   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
 
-val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
+val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT;
 
 (*extract the outer Sucs from a term and convert them to a binary numeral*)
 fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t)
@@ -85,14 +85,14 @@
 (*** CancelNumerals simprocs ***)
 
 val one = mk_numeral 1;
-val mk_times = HOLogic.mk_binop "op *";
+val mk_times = HOLogic.mk_binop "HOL.times";
 
 fun mk_prod [] = one
   | mk_prod [t] = t
   | mk_prod (t :: ts) = if t = one then mk_prod ts
                         else mk_times (t, mk_prod ts);
 
-val dest_times = HOLogic.dest_bin "op *" HOLogic.natT;
+val dest_times = HOLogic.dest_bin "HOL.times" HOLogic.natT;
 
 fun dest_prod t =
       let val (t,u) = dest_times t
@@ -213,8 +213,8 @@
 structure DiffCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Bin_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binop "op -"
-  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT
+  val mk_bal   = HOLogic.mk_binop "HOL.minus"
+  val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT
   val bal_add1 = nat_diff_add_eq1 RS trans
   val bal_add2 = nat_diff_add_eq2 RS trans
 );
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Integ/presburger.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -139,11 +139,11 @@
    ("Divides.op dvd", iT --> iT --> bT),
    ("Divides.op div", iT --> iT --> iT),
    ("Divides.op mod", iT --> iT --> iT),
-   ("op +", iT --> iT --> iT),
-   ("op -", iT --> iT --> iT),
-   ("op *", iT --> iT --> iT), 
+   ("HOL.plus", iT --> iT --> iT),
+   ("HOL.minus", iT --> iT --> iT),
+   ("HOL.times", iT --> iT --> iT), 
    ("HOL.abs", iT --> iT),
-   ("uminus", iT --> iT),
+   ("HOL.uminus", iT --> iT),
    ("HOL.max", iT --> iT --> iT),
    ("HOL.min", iT --> iT --> iT),
 
@@ -153,9 +153,9 @@
    ("Divides.op dvd", nT --> nT --> bT),
    ("Divides.op div", nT --> nT --> nT),
    ("Divides.op mod", nT --> nT --> nT),
-   ("op +", nT --> nT --> nT),
-   ("op -", nT --> nT --> nT),
-   ("op *", nT --> nT --> nT), 
+   ("HOL.plus", nT --> nT --> nT),
+   ("HOL.minus", nT --> nT --> nT),
+   ("HOL.times", nT --> nT --> nT), 
    ("Suc", nT --> nT),
    ("HOL.max", nT --> nT --> nT),
    ("HOL.min", nT --> nT --> nT),
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Integ/reflected_cooper.ML
--- a/src/HOL/Integ/reflected_cooper.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Integ/reflected_cooper.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -16,10 +16,10 @@
       | Const("0",iT) => Cst 0
       | Const("1",iT) => Cst 1
       | Bound i => Var (nat (IntInf.fromInt i))
-      | Const("uminus",_)$t' => Neg (i_of_term vs t')
-      | Const ("op +",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
-      | Const ("op -",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
-      | Const ("op *",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
+      | Const("HOL.uminus",_)$t' => Neg (i_of_term vs t')
+      | Const ("HOL.plus",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
+      | Const ("HOL.minus",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
+      | Const ("HOL.times",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
       | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_binum t')
       | _ => error "i_of_term: unknown term";
 	
@@ -77,12 +77,12 @@
     case t of 
 	Cst i => CooperDec.mk_numeral i
       | Var n => valOf (myassoc2 vs n)
-      | Neg t' => Const("uminus",iT --> iT)$(term_of_i vs t')
-      | Add(t1,t2) => Const("op +",[iT,iT] ---> iT)$
+      | Neg t' => Const("HOL.uminus",iT --> iT)$(term_of_i vs t')
+      | Add(t1,t2) => Const("HOL.plus",[iT,iT] ---> iT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Sub(t1,t2) => Const("op -",[iT,iT] ---> iT)$
+      | Sub(t1,t2) => Const("HOL.minus",[iT,iT] ---> iT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Mult(t1,t2) => Const("op *",[iT,iT] ---> iT)$
+      | Mult(t1,t2) => Const("HOL.times",[iT,iT] ---> iT)$
 			   (term_of_i vs t1)$(term_of_i vs t2);
 
 fun term_of_qf vs t = 
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Library/ExecutableRat.thy
--- a/src/HOL/Library/ExecutableRat.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Library/ExecutableRat.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -15,13 +15,13 @@
 
 datatype erat = Rat bool int int
 
-instance erat :: zero by intro_classes
-instance erat :: one by intro_classes
-instance erat :: plus by intro_classes
-instance erat :: minus by intro_classes
-instance erat :: times by intro_classes
-instance erat :: inverse by intro_classes
-instance erat :: ord by intro_classes
+instance erat :: zero ..
+instance erat :: one ..
+instance erat :: plus ..
+instance erat :: minus ..
+instance erat :: times ..
+instance erat :: inverse ..
+instance erat :: ord ..
 
 consts
   norm :: "erat \<Rightarrow> erat"
@@ -85,12 +85,6 @@
   ml (target_atom "{*erat*}")
   haskell (target_atom "{*erat*}")
 
-code_alias
-  (* an intermediate solution until name resolving of ad-hoc overloaded
-     constants is refined *)
-  "HOL.inverse" "Rational.inverse"
-  "HOL.divide" "Rational.divide"
-
 code_syntax_const
   Fract
     ml ("{*of_quotient*}")
@@ -103,7 +97,7 @@
     haskell ("{*1::erat*}")
   "op + :: rat \<Rightarrow> rat \<Rightarrow> rat"
     ml ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
-    haskell ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
+    haskell ("{*HOL.plus :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
   "uminus :: rat \<Rightarrow> rat"
     ml ("{*uminus :: erat \<Rightarrow> erat*}")
     haskell ("{*uminus :: erat \<Rightarrow> erat*}")
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -40,7 +40,7 @@
   "insert"  ("(_ ins _)")
   "op Un"   ("(_ union _)")
   "op Int"  ("(_ inter _)")
-  "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("(_ \\\\ _)")
+  "HOL.minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("(_ \\\\ _)")
   "image"   ("\<module>image")
 attach {*
 fun image f S = distinct (map f S);
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Library/comm_ring.ML
--- a/src/HOL/Library/comm_ring.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Library/comm_ring.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -77,13 +77,13 @@
 (* reification of polynom expressions *)
 fun reif_polex T vs t =
     case t of
-        Const("op +",_)$a$b => (polex_add T)
+        Const("HOL.plus",_)$a$b => (polex_add T)
                                    $ (reif_polex T vs a)$(reif_polex T vs b)
-      | Const("op -",_)$a$b => (polex_sub T)
+      | Const("HOL.minus",_)$a$b => (polex_sub T)
                                    $ (reif_polex T vs a)$(reif_polex T vs b)
-      | Const("op *",_)$a$b =>  (polex_mul T)
+      | Const("HOL.times",_)$a$b =>  (polex_mul T)
                                     $ (reif_polex T vs a)$ (reif_polex T vs b)
-      | Const("uminus",_)$a => (polex_neg T)
+      | Const("HOL.uminus",_)$a => (polex_neg T)
                                    $ (reif_polex T vs a)
       | (Const("Nat.power",_)$a$n) => (polex_pow T) $ (reif_polex T vs a) $ n
 
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/OrderedGroup.ML
--- a/src/HOL/OrderedGroup.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/OrderedGroup.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -8,7 +8,7 @@
 
 (*** Term order for abelian groups ***)
 
-fun agrp_ord a = find_index_eq a ["0", "op +", "uminus", "op -"];
+fun agrp_ord a = find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus"];
 
 fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
 
@@ -16,9 +16,9 @@
   val ac1 = mk_meta_eq (thm "add_assoc");
   val ac2 = mk_meta_eq (thm "add_commute");
   val ac3 = mk_meta_eq (thm "add_left_commute");
-  fun solve_add_ac thy _ (_ $ (Const ("op +",_) $ _ $ _) $ _) =
+  fun solve_add_ac thy _ (_ $ (Const ("HOL.plus",_) $ _ $ _) $ _) =
         SOME ac1
-    | solve_add_ac thy _ (_ $ x $ (Const ("op +",_) $ y $ z)) =
+    | solve_add_ac thy _ (_ $ x $ (Const ("HOL.plus",_) $ y $ z)) =
         if termless_agrp (y, x) then SOME ac3 else NONE
     | solve_add_ac thy _ (_ $ x $ y) =
         if termless_agrp (y, x) then SOME ac2 else NONE
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/OrderedGroup.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -899,8 +899,7 @@
 lemma abs_triangle_ineq: "abs(a+b) \<le> abs a + abs(b::'a::lordered_ab_group_abs)"
 proof -
   have g:"abs a + abs b = join (a+b) (join (-a-b) (join (-a+b) (a + (-b))))" (is "_=join ?m ?n")
-    apply (simp add: abs_lattice add_meet_join_distribs join_aci)
-    by (simp only: diff_minus)
+    by (simp add: abs_lattice add_meet_join_distribs join_aci diff_minus)
   have a:"a+b <= join ?m ?n" by (simp add: meet_join_le)
   have b:"-a-b <= ?n" by (simp add: meet_join_le) 
   have c:"?n <= join ?m ?n" by (simp add: meet_join_le)
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Real/Float.ML
--- a/src/HOL/Real/Float.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Real/Float.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -330,10 +330,10 @@
 		
 val float_const = Const ("Float.float", HOLogic.mk_prodT (HOLogic.intT, HOLogic.intT) --> HOLogic.realT)
 
-val float_add_const = Const ("op +", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
-val float_diff_const = Const ("op -", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
-val float_mult_const = Const ("op *", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
-val float_uminus_const = Const ("uminus", HOLogic.realT --> HOLogic.realT)
+val float_add_const = Const ("HOL.plus", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
+val float_diff_const = Const ("HOL.minus", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
+val float_mult_const = Const ("HOL.times", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
+val float_uminus_const = Const ("HOL.uminus", HOLogic.realT --> HOLogic.realT)
 val float_abs_const = Const ("HOL.abs", HOLogic.realT --> HOLogic.realT)
 val float_le_const = Const ("op <=", HOLogic.realT --> HOLogic.realT --> HOLogic.boolT)
 val float_pprt_const = Const ("OrderedGroup.pprt", HOLogic.realT --> HOLogic.realT)
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Set.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -958,7 +958,7 @@
   outer-level constant, which in this case is just "op :"; we instead need
   to use term-nets to associate patterns with rules.  Also, if a rule fails to
   apply, then the formula should be kept.
-  [("uminus", Compl_iff RS iffD1), ("op -", [Diff_iff RS iffD1]),
+  [("HOL.uminus", Compl_iff RS iffD1), ("HOL.minus", [Diff_iff RS iffD1]),
    ("op Int", [IntD1,IntD2]),
    ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
  *)
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Tools/Presburger/cooper_dec.ML
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -116,8 +116,8 @@
  
 fun linear_cmul n tm =  if n = 0 then zero else let fun times n k = n*k in  
   ( case tm of  
-     (Const("op +",T)  $  (Const ("op *",T1 ) $c1 $  x1) $ rest) => 
-       Const("op +",T) $ ((Const("op *",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest) 
+     (Const("HOL.plus",T)  $  (Const ("HOL.times",T1 ) $c1 $  x1) $ rest) => 
+       Const("HOL.plus",T) $ ((Const("HOL.times",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest) 
     |_ =>  numeral1 (times n) tm) 
     end ; 
  
@@ -139,23 +139,23 @@
 fun linear_add vars tm1 tm2 = 
   let fun addwith x y = x + y in
  (case (tm1,tm2) of 
-	((Const ("op +",T1) $ ( Const("op *",T2) $ c1 $  x1) $ rest1),(Const 
-	("op +",T3)$( Const("op *",T4) $ c2 $  x2) $ rest2)) => 
+	((Const ("HOL.plus",T1) $ ( Const("HOL.times",T2) $ c1 $  x1) $ rest1),(Const 
+	("HOL.plus",T3)$( Const("HOL.times",T4) $ c2 $  x2) $ rest2)) => 
          if x1 = x2 then 
               let val c = (numeral2 (addwith) c1 c2) 
 	      in 
               if c = zero then (linear_add vars rest1  rest2)  
-	      else (Const("op +",T1) $ (Const("op *",T2) $ c $ x1) $ (linear_add vars  rest1 rest2)) 
+	      else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c $ x1) $ (linear_add vars  rest1 rest2)) 
               end 
 	   else 
-		if earlierv vars x1 x2 then (Const("op +",T1) $  
-		(Const("op *",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2)) 
-    	       else (Const("op +",T1) $ (Const("op *",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2)) 
-   	|((Const("op +",T1) $ (Const("op *",T2) $ c1 $ x1) $ rest1) ,_) => 
-    	  (Const("op +",T1)$ (Const("op *",T2) $ c1 $ x1) $ (linear_add vars 
+		if earlierv vars x1 x2 then (Const("HOL.plus",T1) $  
+		(Const("HOL.times",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2)) 
+    	       else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2)) 
+   	|((Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c1 $ x1) $ rest1) ,_) => 
+    	  (Const("HOL.plus",T1)$ (Const("HOL.times",T2) $ c1 $ x1) $ (linear_add vars 
 	  rest1 tm2)) 
-   	|(_, (Const("op +",T1) $(Const("op *",T2) $ c2 $ x2) $ rest2)) => 
-      	  (Const("op +",T1) $ (Const("op *",T2) $ c2 $ x2) $ (linear_add vars tm1 
+   	|(_, (Const("HOL.plus",T1) $(Const("HOL.times",T2) $ c2 $ x2) $ rest2)) => 
+      	  (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 
 	  rest2)) 
    	| (_,_) => numeral2 (addwith) tm1 tm2) 
 	 
@@ -180,13 +180,13 @@
  Free(x,T)*) 
   
 fun lint vars tm = if is_numeral tm then tm else case tm of 
-   (Free (x,T)) =>  (HOLogic.mk_binop "op +" ((HOLogic.mk_binop "op *" ((mk_numeral 1),Free (x,T))), zero)) 
-  |(Bound i) =>  (Const("op +",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ 
-  (Const("op *",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero) 
-  |(Const("uminus",_) $ t ) => (linear_neg (lint vars t)) 
-  |(Const("op +",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) 
-  |(Const("op -",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) 
-  |(Const ("op *",_) $ s $ t) => 
+   (Free (x,T)) =>  (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1),Free (x,T))), zero)) 
+  |(Bound i) =>  (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ 
+  (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero) 
+  |(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t)) 
+  |(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) 
+  |(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) 
+  |(Const ("HOL.times",_) $ s $ t) => 
         let val s' = lint vars s  
             val t' = lint vars t  
         in 
@@ -212,14 +212,14 @@
       end 
     else (warning "Nonlinear term --- Non numeral leftside at dvd"
       ;raise COOPER)
-  |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
-  |linform vars  (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
-  |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 
+  |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
+  |linform vars  (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
+  |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 
   |linform vars  (Const("op <=",_)$ s $ t ) = 
-        (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("op +",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s)) 
+        (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s)) 
   |linform vars  (Const("op >=",_)$ s $ t ) = 
-        (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> 
-	HOLogic.intT) $ (Const("op +",HOLogic.intT --> HOLogic.intT --> 
+        (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> 
+	HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> 
 	HOLogic.intT) $s $(mk_numeral 1)) $ t)) 
  
    |linform vars  fm =  fm; 
@@ -246,7 +246,7 @@
 fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); 
  
 fun formlcm x fm = case fm of 
-    (Const (p,_)$ _ $(Const ("op +", _)$(Const ("op *",_)$ c $ y ) $z ) ) =>  if 
+    (Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) =>  if 
     (is_arith_rel fm) andalso (x = y) then  (abs(dest_numeral c)) else 1 
   | ( Const ("Not", _) $p) => formlcm x p 
   | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) 
@@ -259,13 +259,13 @@
  
 fun adjustcoeff x l fm = 
      case fm of  
-      (Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $ 
+      (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
       c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
         let val m = l div (dest_numeral c) 
             val n = (if p = "op <" then abs(m) else m) 
-            val xtm = HOLogic.mk_binop "op *" ((mk_numeral (m div n)), x) 
+            val xtm = HOLogic.mk_binop "HOL.times" ((mk_numeral (m div n)), x) 
 	in
-        (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
+        (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
 	end 
 	else fm 
   |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeff x l p) 
@@ -282,8 +282,8 @@
       val fm' = adjustcoeff x l fm in
       if l = 1 then fm' 
 	 else 
-     let val xp = (HOLogic.mk_binop "op +"  
-     		((HOLogic.mk_binop "op *" ((mk_numeral 1), x )), zero))
+     let val xp = (HOLogic.mk_binop "HOL.plus"  
+     		((HOLogic.mk_binop "HOL.times" ((mk_numeral 1), x )), zero))
 	in 
       HOLogic.conj $(HOLogic.mk_binrel "Divides.op dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm) 
       end 
@@ -294,12 +294,12 @@
 (*
 fun adjustcoeffeq x l fm = 
     case fm of  
-      (Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $ 
+      (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
       c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
         let val m = l div (dest_numeral c) 
             val n = (if p = "op <" then abs(m) else m)  
-            val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
-            in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
+            val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
+            in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
 	    end 
 	else fm 
   |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeffeq x l p) 
@@ -315,11 +315,11 @@
 (* ------------------------------------------------------------------------- *) 
  
 fun minusinf x fm = case fm of  
-    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) => 
+    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) => 
   	 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const  
 	 				 else fm 
  
-  |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z 
+  |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z 
   )) => if (x = y) 
 	then if (pm1 = one) andalso (c = zero) then HOLogic.false_const 
 	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
@@ -336,11 +336,11 @@
 (* ------------------------------------------------------------------------- *)
 
 fun plusinf x fm = case fm of
-    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
+    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
   	 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
 	 				 else fm
 
-  |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z
+  |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
   )) => if (x = y) 
 	then if (pm1 = one) andalso (c = zero) then HOLogic.true_const 
 	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
@@ -356,7 +356,7 @@
 (* The LCM of all the divisors that involve x.                               *) 
 (* ------------------------------------------------------------------------- *) 
  
-fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z ) ) =  
+fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =  
         if x = y then abs(dest_numeral d) else 1 
   |divlcm x ( Const ("Not", _) $ p) = divlcm x p 
   |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q) 
@@ -370,15 +370,15 @@
 fun bset x fm = case fm of 
    (Const ("Not", _) $ p) => if (is_arith_rel p) then  
           (case p of  
-	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $c2 $y) $a ) )  
+	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )  
 	             => if (is_arith_rel p) andalso (x=	y) andalso (c2 = one) andalso (c1 = zero)  
 	                then [linear_neg a] 
 			else  bset x p 
    	  |_ =>[]) 
 			 
 			else bset x p 
-  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +",_) $ (Const ("op *",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))]  else [] 
-  |(Const ("op <",_) $ c1$ (Const ("op +",_) $(Const ("op *",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] 
+  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))]  else [] 
+  |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] 
   |(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q) 
   |(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q) 
   |_ => []; 
@@ -390,15 +390,15 @@
 fun aset x fm = case fm of
    (Const ("Not", _) $ p) => if (is_arith_rel p) then
           (case p of
-	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $c2 $y) $a ) )
+	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )
 	             => if (x=	y) andalso (c2 = one) andalso (c1 = zero)
 	                then [linear_neg a]
 			else  []
    	  |_ =>[])
 
 			else aset x p
-  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +",_) $ (Const ("op *",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a]  else []
-  |(Const ("op <",_) $ c1$ (Const ("op +",_) $(Const ("op *",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
+  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a]  else []
+  |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
   |(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
   |(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
   |_ => [];
@@ -409,7 +409,7 @@
 (* ------------------------------------------------------------------------- *) 
  
 fun linrep vars x t fm = case fm of  
-   ((Const(p,_)$ d $ (Const("op +",_)$(Const("op *",_)$ c $ y) $ z))) => 
+   ((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) => 
       if (x = y) andalso (is_arith_rel fm)  
       then  
         let val ct = linear_cmul (dest_numeral c) t  
@@ -435,8 +435,8 @@
    val dn = dest_numeral d
    fun coeffs_of x = case x of 
      Const(p,_) $ tl $ tr => 
-       if p = "op +" then (coeffs_of tl) union (coeffs_of tr)
-          else if p = "op *" 
+       if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr)
+          else if p = "HOL.times" 
 	        then if (is_numeral tr) 
 		 then [(dest_numeral tr) * (dest_numeral tl)] 
 		 else [dest_numeral tl]
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Tools/Presburger/cooper_proof.ML
--- a/src/HOL/Tools/Presburger/cooper_proof.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -165,11 +165,11 @@
 (* ------------------------------------------------------------------------- *)
 
 fun norm_zero_one fm = case fm of
-  (Const ("op *",_) $ c $ t) => 
+  (Const ("HOL.times",_) $ c $ t) => 
     if c = one then (norm_zero_one t)
     else if (dest_numeral c = ~1) 
-         then (Const("uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
-         else (HOLogic.mk_binop "op *" (norm_zero_one c,norm_zero_one t))
+         then (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
+         else (HOLogic.mk_binop "HOL.times" (norm_zero_one c,norm_zero_one t))
   |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
   |(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
   |_ => fm;
@@ -255,13 +255,13 @@
 (*==================================================*)
 
 fun decomp_adjustcoeffeq sg x l fm = case fm of
-    (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("op +", _)$(Const ("op *",_) $    c $ y ) $z )))) => 
+    (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $    c $ y ) $z )))) => 
      let  
         val m = l div (dest_numeral c) 
         val n = if (x = y) then abs (m) else 1
-        val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x)) 
+        val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x)) 
         val rs = if (x = y) 
-                 then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
+                 then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
                  else HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )
         val ck = cterm_of sg (mk_numeral n)
         val cc = cterm_of sg c
@@ -273,14 +273,14 @@
         in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
         end
 
-  |(Const(p,_) $a $( Const ("op +", _)$(Const ("op *",_) $ 
+  |(Const(p,_) $a $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
       c $ y ) $t )) => 
    if (is_arith_rel fm) andalso (x = y) 
    then  
         let val m = l div (dest_numeral c) 
            val k = (if p = "op <" then abs(m) else m)  
-           val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div k)*l) ), x))
-           val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul k t) )))) 
+           val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div k)*l) ), x))
+           val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) )))) 
 
            val ck = cterm_of sg (mk_numeral k)
            val cc = cterm_of sg c
@@ -335,28 +335,28 @@
    val cfalse = cterm_of sg HOLogic.false_const
    val fm = norm_zero_one fm1
   in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
+      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
          if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
            else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
 
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
+      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
   	   if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one) 
 	   then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf))
 	 	 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) 
 
-      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
+      |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
            if (y=x) andalso (c1 = zero) then 
             if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else
 	     (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
   
-      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
 			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
-      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
+      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
       c $ y ) $ z))) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
 			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
@@ -373,22 +373,22 @@
    let
    val fm = norm_zero_one fm1
     in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
+      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
          if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	   then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
            else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
 
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
+      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
   	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
 	     then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
 	     else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) 
 
-      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
+      |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
            if (y=x) andalso (c1 =zero) then 
             if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
 	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
-      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_minf)) 
@@ -396,7 +396,7 @@
 
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
 		
-      |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+      |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf))
@@ -431,30 +431,30 @@
   val cfalse = cterm_of sg HOLogic.false_const
   val fm = norm_zero_one fm1
  in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
+      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
          if ((x=y) andalso (c1= zero) andalso (c2= one))
 	 then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
          else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
 
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
+      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
   	if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero)  andalso (c2 = one)) 
 	then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
 	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
 
-      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
+      |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
         if ((y=x) andalso (c1 = zero)) then 
           if (pm1 = one) 
 	  then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf)) 
 	  else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
 	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
   
-      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
 			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
-      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
+      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
       c $ y ) $ z))) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
 			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
@@ -472,22 +472,22 @@
   let
 					val fm = norm_zero_one fm1
     in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
+      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
          if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	   then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
            else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
 
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
+      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
   	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
 	     then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
 	     else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) 
 
-      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
+      |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
            if (y=x) andalso (c1 =zero) then 
             if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
 	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
-      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_pinf)) 
@@ -495,7 +495,7 @@
 
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
 		
-      |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+      |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf))
@@ -567,31 +567,31 @@
     val cat = cterm_of sg (norm_zero_one at)
   in
   case at of 
-   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
+   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
       if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
-	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
+	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
 		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
 	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
 	 end
          else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
+   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
      if (is_arith_rel at) andalso (x=y)
 	then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
 	         in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
-	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("op -",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
+	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
 		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
 	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
 	 end
        end
          else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
+   |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
         if (y=x) andalso (c1 =zero) then 
         if pm1 = one then 
 	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
-              val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
+              val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
 	  in  (instantiate' [] [SOME cfma,  SOME cdlcm]([th1,th2] MRS (not_bst_p_gt)))
 	    end
 	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
@@ -599,7 +599,7 @@
 	      end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
       if y=x then  
            let val cz = cterm_of sg (norm_zero_one z)
 	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
@@ -607,7 +607,7 @@
 	     end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+   |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
        if y=x then  
 	 let val cz = cterm_of sg (norm_zero_one z)
 	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
@@ -658,26 +658,26 @@
     val cat = cterm_of sg (norm_zero_one at)
   in
   case at of 
-   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
+   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
       if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A)
-	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
+	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
 		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
 	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
 	 end
          else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
+   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
      if (is_arith_rel at) andalso (x=y)
 	then let val ast_z = norm_zero_one (linear_sub [] one z )
 	         val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
-	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("op +",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
+	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("HOL.plus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
 		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
 	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
        end
          else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
+   |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
         if (y=x) andalso (c1 =zero) then 
         if pm1 = (mk_numeral ~1) then 
 	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
@@ -689,7 +689,7 @@
 	      end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
       if y=x then  
            let val cz = cterm_of sg (norm_zero_one z)
 	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
@@ -697,7 +697,7 @@
 	     end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
+   |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
        if y=x then  
 	 let val cz = cterm_of sg (norm_zero_one z)
 	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Tools/Presburger/presburger.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -139,11 +139,11 @@
    ("Divides.op dvd", iT --> iT --> bT),
    ("Divides.op div", iT --> iT --> iT),
    ("Divides.op mod", iT --> iT --> iT),
-   ("op +", iT --> iT --> iT),
-   ("op -", iT --> iT --> iT),
-   ("op *", iT --> iT --> iT), 
+   ("HOL.plus", iT --> iT --> iT),
+   ("HOL.minus", iT --> iT --> iT),
+   ("HOL.times", iT --> iT --> iT), 
    ("HOL.abs", iT --> iT),
-   ("uminus", iT --> iT),
+   ("HOL.uminus", iT --> iT),
    ("HOL.max", iT --> iT --> iT),
    ("HOL.min", iT --> iT --> iT),
 
@@ -153,9 +153,9 @@
    ("Divides.op dvd", nT --> nT --> bT),
    ("Divides.op div", nT --> nT --> nT),
    ("Divides.op mod", nT --> nT --> nT),
-   ("op +", nT --> nT --> nT),
-   ("op -", nT --> nT --> nT),
-   ("op *", nT --> nT --> nT), 
+   ("HOL.plus", nT --> nT --> nT),
+   ("HOL.minus", nT --> nT --> nT),
+   ("HOL.times", nT --> nT --> nT), 
    ("Suc", nT --> nT),
    ("HOL.max", nT --> nT --> nT),
    ("HOL.min", nT --> nT --> nT),
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Tools/Presburger/reflected_cooper.ML
--- a/src/HOL/Tools/Presburger/reflected_cooper.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Tools/Presburger/reflected_cooper.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -16,10 +16,10 @@
       | Const("0",iT) => Cst 0
       | Const("1",iT) => Cst 1
       | Bound i => Var (nat (IntInf.fromInt i))
-      | Const("uminus",_)$t' => Neg (i_of_term vs t')
-      | Const ("op +",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
-      | Const ("op -",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
-      | Const ("op *",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
+      | Const("HOL.uminus",_)$t' => Neg (i_of_term vs t')
+      | Const ("HOL.plus",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
+      | Const ("HOL.minus",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
+      | Const ("HOL.times",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
       | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_binum t')
       | _ => error "i_of_term: unknown term";
 	
@@ -77,12 +77,12 @@
     case t of 
 	Cst i => CooperDec.mk_numeral i
       | Var n => valOf (myassoc2 vs n)
-      | Neg t' => Const("uminus",iT --> iT)$(term_of_i vs t')
-      | Add(t1,t2) => Const("op +",[iT,iT] ---> iT)$
+      | Neg t' => Const("HOL.uminus",iT --> iT)$(term_of_i vs t')
+      | Add(t1,t2) => Const("HOL.plus",[iT,iT] ---> iT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Sub(t1,t2) => Const("op -",[iT,iT] ---> iT)$
+      | Sub(t1,t2) => Const("HOL.minus",[iT,iT] ---> iT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Mult(t1,t2) => Const("op *",[iT,iT] ---> iT)$
+      | Mult(t1,t2) => Const("HOL.times",[iT,iT] ---> iT)$
 			   (term_of_i vs t1)$(term_of_i vs t2);
 
 fun term_of_qf vs t = 
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -404,7 +404,7 @@
     val def_names = map (fn s => s ^ "_def") (DatatypeProp.indexify_names
       (map (fn T => name_of_typ T ^ "_size") recTs));
 
-    fun plus (t1, t2) = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
+    fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
 
     fun make_sizefun (_, cargs) =
       let
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Tools/datatype_prop.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -366,7 +366,7 @@
     val size_consts = map (fn (s, T) =>
       Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
 
-    fun plus (t1, t2) = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
+    fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
 
     fun make_size_eqn size_const T (cname, cargs) =
       let
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Tools/refute.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -622,9 +622,9 @@
 			| Const ("Finite_Set.card", T)    => collect_type_axioms (axs, T)
 			| Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T)
 			| Const ("op <", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => collect_type_axioms (axs, T)
-			| Const ("op +", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
-			| Const ("op -", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
-			| Const ("op *", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
+			| Const ("HOL.plus", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
+			| Const ("HOL.minus", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
+			| Const ("HOL.times", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
 			| Const ("List.op @", T)          => collect_type_axioms (axs, T)
 			| Const ("Lfp.lfp", T)            => collect_type_axioms (axs, T)
 			| Const ("Gfp.gfp", T)            => collect_type_axioms (axs, T)
@@ -2162,13 +2162,13 @@
 
 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
 
-	(* only an optimization: 'op +' could in principle be interpreted with    *)
+	(* only an optimization: 'HOL.plus' could in principle be interpreted with*)
 	(* interpreters available already (using its definition), but the code    *)
 	(* below is more efficient                                                *)
 
 	fun Nat_plus_interpreter thy model args t =
 		case t of
-		  Const ("op +", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
+		  Const ("HOL.plus", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
 			let
 				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
 				val size_nat      = size_of_type i_nat
@@ -2196,7 +2196,7 @@
 
 	fun Nat_minus_interpreter thy model args t =
 		case t of
-		  Const ("op -", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
+		  Const ("HOL.minus", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
 			let
 				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
 				val size_nat      = size_of_type i_nat
@@ -2215,13 +2215,13 @@
 
 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
 
-	(* only an optimization: 'op *' could in principle be interpreted with    *)
-	(* interpreters available already (using its definition), but the code    *)
-	(* below is more efficient                                                *)
+	(* only an optimization: 'HOL.times' could in principle be interpreted with *)
+	(* interpreters available already (using its definition), but the code      *)
+	(* below is more efficient                                                  *)
 
 	fun Nat_mult_interpreter thy model args t =
 		case t of
-		  Const ("op *", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
+		  Const ("HOL.times", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
 			let
 				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
 				val size_nat      = size_of_type i_nat
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Tools/res_clause.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -94,9 +94,9 @@
 		   ("op <", "less"),
 		   ("op &", "and"),
 		   ("op |", "or"),
-		   ("op +", "plus"),
-		   ("op -", "minus"),
-		   ("op *", "times"),
+		   ("HOL.plus", "plus"),
+		   ("HOL.minus", "minus"),
+		   ("HOL.times", "times"),
 		   ("Divides.op div", "div"),
 		   ("HOL.divide", "divide"),
 		   ("op -->", "implies"),
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/arith_data.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -17,7 +17,7 @@
 (* mk_sum, mk_norm_sum *)
 
 val one = HOLogic.mk_nat 1;
-val mk_plus = HOLogic.mk_binop "op +";
+val mk_plus = HOLogic.mk_binop "HOL.plus";
 
 fun mk_sum [] = HOLogic.zero
   | mk_sum [t] = t
@@ -32,7 +32,7 @@
 
 (* dest_sum *)
 
-val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
+val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT;
 
 fun dest_sum tm =
   if HOLogic.is_zero tm then []
@@ -137,8 +137,8 @@
 structure DiffCancelSums = CancelSumsFun
 (struct
   open Sum;
-  val mk_bal = HOLogic.mk_binop "op -";
-  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT;
+  val mk_bal = HOLogic.mk_binop "HOL.minus";
+  val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT;
   val uncancel_tac = gen_uncancel_tac diff_cancel;
 end);
 
@@ -267,14 +267,14 @@
 
 fun demult inj_consts =
 let
-fun demult((mC as Const("op *",_)) $ s $ t,m) = ((case s of
+fun demult((mC as Const("HOL.times",_)) $ s $ t,m) = ((case s of
         Const("Numeral.number_of",_)$n
         => demult(t,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum n)))
-      | Const("uminus",_)$(Const("Numeral.number_of",_)$n)
+      | Const("HOL.uminus",_)$(Const("Numeral.number_of",_)$n)
         => demult(t,Rat.mult(m,Rat.rat_of_intinf(~(HOLogic.dest_binum n))))
       | Const("Suc",_) $ _
         => demult(t,Rat.mult(m,Rat.rat_of_int(number_of_Sucs s)))
-      | Const("op *",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m)
+      | Const("HOL.times",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m)
       | Const("HOL.divide",_) $ numt $ (Const("Numeral.number_of",_)$dent) =>
           let val den = HOLogic.dest_binum dent
           in if den = 0 then raise Zero
@@ -291,7 +291,7 @@
   | demult(t as Const("Numeral.number_of",_)$n,m) =
       ((NONE,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum n)))
        handle TERM _ => (SOME t,m))
-  | demult(Const("uminus",_)$t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1)))
+  | demult(Const("HOL.uminus",_)$t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1)))
   | demult(t as Const f $ x, m) =
       (if f mem inj_consts then SOME x else SOME t,m)
   | demult(atom,m) = (SOME atom,m)
@@ -303,15 +303,15 @@
 fun decomp2 inj_consts (rel,lhs,rhs) =
 let
 (* Turn term into list of summand * multiplicity plus a constant *)
-fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
-  | poly(all as Const("op -",T) $ s $ t, m, pi) =
+fun poly(Const("HOL.plus",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
+  | poly(all as Const("HOL.minus",T) $ s $ t, m, pi) =
       if nT T then add_atom(all,m,pi) else poly(s,m,poly(t,Rat.neg m,pi))
-  | poly(all as Const("uminus",T) $ t, m, pi) =
+  | poly(all as Const("HOL.uminus",T) $ t, m, pi) =
       if nT T then add_atom(all,m,pi) else poly(t,Rat.neg m,pi)
   | poly(Const("0",_), _, pi) = pi
   | poly(Const("1",_), m, (p,i)) = (p,Rat.add(i,m))
   | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,Rat.add(i,m)))
-  | poly(t as Const("op *",_) $ _ $ _, m, pi as (p,i)) =
+  | poly(t as Const("HOL.times",_) $ _ $ _, m, pi as (p,i)) =
       (case demult inj_consts (t,m) of
          (NONE,m') => (p,Rat.add(i,m))
        | (SOME u,m') => add_atom(u,m',pi))
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/ex/SVC_Oracle.ML
--- a/src/HOL/ex/SVC_Oracle.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/ex/SVC_Oracle.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -46,21 +46,21 @@
       | lit (t as Const("Numeral.number_of", _) $ w) = t
       | lit t = replace t
     (*abstraction of a real/rational expression*)
-    fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y)
-      | rat ((c as Const("op -", _)) $ x $ y) = c $ (rat x) $ (rat y)
-      | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y)
-      | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y)
-      | rat ((c as Const("uminus", _)) $ x) = c $ (rat x)
+    fun rat ((c as Const("HOL.plus", _)) $ x $ y) = c $ (rat x) $ (rat y)
+      | rat ((c as Const("HOL.minus", _)) $ x $ y) = c $ (rat x) $ (rat y)
+      | rat ((c as Const("HOL.divide", _)) $ x $ y) = c $ (rat x) $ (rat y)
+      | rat ((c as Const("HOL.times", _)) $ x $ y) = c $ (rat x) $ (rat y)
+      | rat ((c as Const("HOL.uminus", _)) $ x) = c $ (rat x)
       | rat t = lit t
     (*abstraction of an integer expression: no div, mod*)
-    fun int ((c as Const("op +", _)) $ x $ y) = c $ (int x) $ (int y)
-      | int ((c as Const("op -", _)) $ x $ y) = c $ (int x) $ (int y)
-      | int ((c as Const("op *", _)) $ x $ y) = c $ (int x) $ (int y)
-      | int ((c as Const("uminus", _)) $ x) = c $ (int x)
+    fun int ((c as Const("HOL.plus", _)) $ x $ y) = c $ (int x) $ (int y)
+      | int ((c as Const("HOL.minus", _)) $ x $ y) = c $ (int x) $ (int y)
+      | int ((c as Const("HOL.times", _)) $ x $ y) = c $ (int x) $ (int y)
+      | int ((c as Const("HOL.uminus", _)) $ x) = c $ (int x)
       | int t = lit t
     (*abstraction of a natural number expression: no minus*)
-    fun nat ((c as Const("op +", _)) $ x $ y) = c $ (nat x) $ (nat y)
-      | nat ((c as Const("op *", _)) $ x $ y) = c $ (nat x) $ (nat y)
+    fun nat ((c as Const("HOL.plus", _)) $ x $ y) = c $ (nat x) $ (nat y)
+      | nat ((c as Const("HOL.times", _)) $ x $ y) = c $ (nat x) $ (nat y)
       | nat ((c as Const("Suc", _)) $ x) = c $ (nat x)
       | nat t = lit t
     (*abstraction of a relation: =, <, <=*)
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/ex/mesontest2.ML
--- a/src/HOL/ex/mesontest2.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/ex/mesontest2.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -547,9 +547,9 @@
 \  (has(p4::'a,goto(out))) &        \
 \  (follows(p5::'a,p4)) &   \
 \  (follows(p6::'a,p3)) &   \
-\  (has(p6::'a,assign(register_k::'a,times(num2::'a,register_k)))) &   \
+\  (has(p6::'a,assign(register_k::'a,mtimes(num2::'a,register_k)))) &   \
 \  (follows(p7::'a,p6)) &   \
-\  (has(p7::'a,assign(register_j::'a,plus(register_j::'a,num1)))) &    \
+\  (has(p7::'a,assign(register_j::'a,mplus(register_j::'a,num1)))) &    \
 \  (follows(p8::'a,p7)) &   \
 \  (has(p8::'a,goto(loop))) &       \
 \  (~succeeds(p3::'a,p3)) --> False",
@@ -570,9 +570,9 @@
 \  (has(p4::'a,goto(out))) &        \
 \  (follows(p5::'a,p4)) &   \
 \  (follows(p6::'a,p3)) &   \
-\  (has(p6::'a,assign(register_k::'a,times(num2::'a,register_k)))) &   \
+\  (has(p6::'a,assign(register_k::'a,mtimes(num2::'a,register_k)))) &   \
 \  (follows(p7::'a,p6)) &   \
-\  (has(p7::'a,assign(register_j::'a,plus(register_j::'a,num1)))) &    \
+\  (has(p7::'a,assign(register_j::'a,mplus(register_j::'a,num1)))) &    \
 \  (follows(p8::'a,p7)) &   \
 \  (has(p8::'a,goto(loop))) &       \
 \  (fails(p3::'a,p3)) --> False",
@@ -768,7 +768,6 @@
 \  (\\<forall>X V1 V2 V3 V4 Y V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,X,V5),continuous(V1::'a,V2,V3,V4,Y,V5))) &    \
 \  (\\<forall>X V1 V2 V3 V4 V5 Y. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,V5,X),continuous(V1::'a,V2,V3,V4,V5,Y)))";
 
-
 (*4272 inferences so far.  Searching to depth 10.  29.4 secs*)
 val GEO017_2 = prove_hard
  (EQU001_0_ax ^ "&" ^ GEO002_ax_eq ^ "  &    \
@@ -1224,26 +1223,26 @@
 
 (*73 inferences so far.  Searching to depth 10.  0.2 secs*)
 val MSC003_1 = prove
- ("(\\<forall>Number_of_small_parts Small_part Big_part Number_of_mid_parts Mid_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) --> in'(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Mid_part) | has_parts(Big_part::'a,times(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &        \
-\  (\\<forall>Big_part Mid_part Number_of_mid_parts Number_of_small_parts Small_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) & has_parts(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Number_of_small_parts,Small_part) --> has_parts(Big_part::'a,times(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &   \
+ ("(\\<forall>Number_of_small_parts Small_part Big_part Number_of_mid_parts Mid_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) --> in'(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Mid_part) | has_parts(Big_part::'a,mtimes(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &        \
+\  (\\<forall>Big_part Mid_part Number_of_mid_parts Number_of_small_parts Small_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) & has_parts(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Number_of_small_parts,Small_part) --> has_parts(Big_part::'a,mtimes(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &   \
 \  (in'(john::'a,boy)) &    \
 \  (\\<forall>X. in'(X::'a,boy) --> in'(X::'a,human)) & \
 \  (\\<forall>X. in'(X::'a,hand) --> has_parts(X::'a,num5,fingers)) &      \
 \  (\\<forall>X. in'(X::'a,human) --> has_parts(X::'a,num2,arm)) & \
 \  (\\<forall>X. in'(X::'a,arm) --> has_parts(X::'a,num1,hand)) &  \
-\  (~has_parts(john::'a,times(num2::'a,num1),hand)) --> False",
+\  (~has_parts(john::'a,mtimes(num2::'a,num1),hand)) --> False",
   meson_tac 1);
 
 (*1486 inferences so far.  Searching to depth 20.  1.2 secs*)
 val MSC004_1 = prove
- ("(\\<forall>Number_of_small_parts Small_part Big_part Number_of_mid_parts Mid_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) --> in'(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Mid_part) | has_parts(Big_part::'a,times(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &        \
-\  (\\<forall>Big_part Mid_part Number_of_mid_parts Number_of_small_parts Small_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) & has_parts(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Number_of_small_parts,Small_part) --> has_parts(Big_part::'a,times(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &   \
+ ("(\\<forall>Number_of_small_parts Small_part Big_part Number_of_mid_parts Mid_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) --> in'(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Mid_part) | has_parts(Big_part::'a,mtimes(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &        \
+\  (\\<forall>Big_part Mid_part Number_of_mid_parts Number_of_small_parts Small_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) & has_parts(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Number_of_small_parts,Small_part) --> has_parts(Big_part::'a,mtimes(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &   \
 \  (in'(john::'a,boy)) &    \
 \  (\\<forall>X. in'(X::'a,boy) --> in'(X::'a,human)) & \
 \  (\\<forall>X. in'(X::'a,hand) --> has_parts(X::'a,num5,fingers)) &      \
 \  (\\<forall>X. in'(X::'a,human) --> has_parts(X::'a,num2,arm)) & \
 \  (\\<forall>X. in'(X::'a,arm) --> has_parts(X::'a,num1,hand)) &  \
-\  (~has_parts(john::'a,times(times(num2::'a,num1),num5),fingers)) --> False",
+\  (~has_parts(john::'a,mtimes(mtimes(num2::'a,num1),num5),fingers)) --> False",
   meson_tac 1);
 
 (*100 inferences so far.  Searching to depth 12.  0.1 secs*)
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/ex/svc_funcs.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -154,16 +154,16 @@
       | lit (Const("0", _)) = 0
       | lit (Const("1", _)) = 1
     (*translation of a literal expression [no variables]*)
-    fun litExp (Const("op +", T) $ x $ y) =
+    fun litExp (Const("HOL.plus", T) $ x $ y) =
           if is_numeric_op T then (litExp x) + (litExp y)
           else fail t
-      | litExp (Const("op -", T) $ x $ y) =
+      | litExp (Const("HOL.minus", T) $ x $ y) =
           if is_numeric_op T then (litExp x) - (litExp y)
           else fail t
-      | litExp (Const("op *", T) $ x $ y) =
+      | litExp (Const("HOL.times", T) $ x $ y) =
           if is_numeric_op T then (litExp x) * (litExp y)
           else fail t
-      | litExp (Const("uminus", T) $ x)   =
+      | litExp (Const("HOL.uminus", T) $ x)   =
           if is_numeric_op T then ~(litExp x)
           else fail t
       | litExp t = lit t
@@ -171,21 +171,21 @@
     (*translation of a real/rational expression*)
     fun suc t = Interp("+", [Int 1, t])
     fun tm (Const("Suc", T) $ x) = suc (tm x)
-      | tm (Const("op +", T) $ x $ y) =
+      | tm (Const("HOL.plus", T) $ x $ y) =
           if is_numeric_op T then Interp("+", [tm x, tm y])
           else fail t
-      | tm (Const("op -", T) $ x $ y) =
+      | tm (Const("HOL.minus", T) $ x $ y) =
           if is_numeric_op T then
               Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
           else fail t
-      | tm (Const("op *", T) $ x $ y) =
+      | tm (Const("HOL.times", T) $ x $ y) =
           if is_numeric_op T then Interp("*", [tm x, tm y])
           else fail t
       | tm (Const("RealDef.rinv", T) $ x) =
           if domain_type T = HOLogic.realT then
               Rat(1, litExp x)
           else fail t
-      | tm (Const("uminus", T) $ x) =
+      | tm (Const("HOL.uminus", T) $ x) =
           if is_numeric_op T then Interp("*", [Int ~1, tm x])
           else fail t
       | tm t = Int (lit t)
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/Provers/Arith/abel_cancel.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -31,28 +31,28 @@
 open Data;
 
  fun zero t = Const ("0", t);
- fun minus t = Const ("uminus", t --> t);
+ fun minus t = Const ("HOL.uminus", t --> t);
 
- fun add_terms pos (Const ("op +", _) $ x $ y, ts) =
+ fun add_terms pos (Const ("HOL.plus", _) $ x $ y, ts) =
          add_terms pos (x, add_terms pos (y, ts))
-   | add_terms pos (Const ("op -", _) $ x $ y, ts) =
+   | add_terms pos (Const ("HOL.minus", _) $ x $ y, ts) =
          add_terms pos (x, add_terms (not pos) (y, ts))
-   | add_terms pos (Const ("uminus", _) $ x, ts) =
+   | add_terms pos (Const ("HOL.uminus", _) $ x, ts) =
          add_terms (not pos) (x, ts)
    | add_terms pos (x, ts) = (pos,x) :: ts;
 
  fun terms fml = add_terms true (fml, []);
 
-fun zero1 pt (u as (c as Const("op +",_)) $ x $ y) =
+fun zero1 pt (u as (c as Const("HOL.plus",_)) $ x $ y) =
       (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
                                    | SOME z => SOME(c $ x $ z))
        | SOME z => SOME(c $ z $ y))
-  | zero1 (pos,t) (u as (c as Const("op -",_)) $ x $ y) =
+  | zero1 (pos,t) (u as (c as Const("HOL.minus",_)) $ x $ y) =
       (case zero1 (pos,t) x of
          NONE => (case zero1 (not pos,t) y of NONE => NONE
                   | SOME z => SOME(c $ x $ z))
        | SOME z => SOME(c $ z $ y))
-  | zero1 (pos,t) (u as (c as Const("uminus",_)) $ x) =
+  | zero1 (pos,t) (u as (c as Const("HOL.uminus",_)) $ x) =
       (case zero1 (not pos,t) x of NONE => NONE
        | SOME z => SOME(c $ z))
   | zero1 (pos,t) u =
@@ -77,7 +77,7 @@
               then tracing ("Abel cancel: " ^ string_of_cterm (cterm_of sg t))
               else ()
       val c $ lhs $ rhs = t
-      val opp = case c of Const("op +",_) => true | _ => false;
+      val opp = case c of Const("HOL.plus",_) => true | _ => false;
       val (pos,l) = find_common opp (terms lhs) (terms rhs)
       val posr = if opp then not pos else pos
       val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs))
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/Provers/Arith/cancel_div_mod.ML
--- a/src/Provers/Arith/cancel_div_mod.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/Provers/Arith/cancel_div_mod.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -6,8 +6,8 @@
 
   A + n*(m div n) + B + (m mod n) + C  ==  A + B + C + m
 
-Is parameterized but assumes for simplicity that + and * are called
-"op +" and "op *"
+FIXME: Is parameterized but assumes for simplicity that + and * are called
+"HOL.plus" and "HOL.minus"
 *)
 
 signature CANCEL_DIV_MOD_DATA =
@@ -35,12 +35,12 @@
 functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
 struct
 
-fun coll_div_mod (Const("op +",_) $ s $ t) dms =
+fun coll_div_mod (Const("HOL.plus",_) $ s $ t) dms =
       coll_div_mod t (coll_div_mod s dms)
-  | coll_div_mod (Const("op *",_) $ m $ (Const(d,_) $ s $ n))
+  | coll_div_mod (Const("HOL.times",_) $ m $ (Const(d,_) $ s $ n))
                  (dms as (divs,mods)) =
       if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
-  | coll_div_mod (Const("op *",_) $ (Const(d,_) $ s $ n) $ m)
+  | coll_div_mod (Const("HOL.times",_) $ (Const(d,_) $ s $ n) $ m)
                  (dms as (divs,mods)) =
       if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
   | coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =
@@ -56,8 +56,8 @@
    ==> thesis by transitivity
 *)
 
-val mk_plus = Data.mk_binop "op +"
-val mk_times = Data.mk_binop "op *"
+val mk_plus = Data.mk_binop "HOL.plus"
+val mk_times = Data.mk_binop "HOL.times"
 
 fun rearrange t pq =
   let val ts = Data.dest_sum t;
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -623,18 +623,10 @@
     val typ_def = Type.varifyT raw_typ_def;
     val typ_use = Type.varifyT raw_typ_use;
     val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty;
-    fun get_first_index f =
-      let
-        fun get _ [] = NONE
-          | get i (x::xs) = 
-              case f x
-               of NONE => get (i+1) xs
-                | SOME y => SOME (i, y)
-      in get 0 end;
     fun tab_lookup vname = (the o Vartab.lookup match_tab) (vname, 0);
     fun mk_class_deriv thy subclasses superclass =
       let
-        val (i, (subclass::deriv)) = (the oo get_first_index) (fn subclass =>
+        val (i, (subclass::deriv)) = (the oo get_index) (fn subclass =>
             get_superclass_derivation thy (subclass, superclass)
           ) subclasses;
         val i' = if length subclasses = 1 then ~1 else i;
diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/Pure/library.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -126,6 +126,7 @@
   val find_index: ('a -> bool) -> 'a list -> int
   val find_index_eq: ''a -> ''a list -> int
   val find_first: ('a -> bool) -> 'a list -> 'a option
+  val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
   val get_first: ('a -> 'b option) -> 'a list -> 'b option
   val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
@@ -632,6 +633,15 @@
         NONE => get_first f xs
       | some => some);
 
+fun get_index f =
+  let
+    fun get _ [] = NONE
+      | get i (x::xs) = 
+          case f x
+           of NONE => get (i+1) xs
+            | SOME y => SOME (i, y)
+  in get 0 end;
+
 (*flatten a list of lists to a list*)
 val flat = List.concat;