# HG changeset patch
# User haftmann
# Date 1264675729 -3600
# Node ID 18b41bba42b59f637c01244fd43c739dc64080ea
# Parent  ae634fad947e3a8c67340d058edafac070ef632f
new theory Algebras.thy for generic algebraic structures

diff -r ae634fad947e -r 18b41bba42b5 NEWS
--- a/NEWS	Thu Jan 28 11:48:43 2010 +0100
+++ b/NEWS	Thu Jan 28 11:48:49 2010 +0100
@@ -12,6 +12,11 @@
 
 *** HOL ***
 
+* new theory Algebras.thy contains generic algebraic structures and
+generic algebraic operations.  INCOMPATIBILTY: constants zero, one,
+plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and less
+have been moved from HOL.thy to Algebras.thy.
+
 * HOLogic.strip_psplit: types are returned in syntactic order, similar
 to other strip and tuple operations.  INCOMPATIBILITY.
 
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -205,8 +205,8 @@
 ML {*
 fun ring_ord (Const (a, _)) =
     find_index (fn a' => a = a')
-      [@{const_name HOL.zero}, @{const_name HOL.plus}, @{const_name HOL.uminus},
-        @{const_name HOL.minus}, @{const_name HOL.one}, @{const_name HOL.times}]
+      [@{const_name Algebras.zero}, @{const_name Algebras.plus}, @{const_name Algebras.uminus},
+        @{const_name Algebras.minus}, @{const_name Algebras.one}, @{const_name Algebras.times}]
   | ring_ord _ = ~1;
 
 fun termless_ring (a, b) = (TermOrd.term_lpo ring_ord (a, b) = LESS);
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Algebras.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebras.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -0,0 +1,166 @@
+(*  Title:      HOL/Algebras.thy
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* Generic algebraic structures and operations *}
+
+theory Algebras
+imports HOL
+begin
+
+subsection {* Generic algebraic structures *}
+
+locale semigroup =
+  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
+  assumes assoc: "a * b * c = a * (b * c)"
+
+locale abel_semigroup = semigroup +
+  assumes commute: "a * b = b * a"
+begin
+
+lemma left_commute:
+  "b * (a * c) = a * (b * c)"
+proof -
+  have "(b * a) * c = (a * b) * c"
+    by (simp only: commute)
+  then show ?thesis
+    by (simp only: assoc)
+qed
+
+end
+
+locale semilattice = abel_semigroup +
+  assumes idem [simp]: "a * a = a"
+begin
+
+lemma left_idem [simp]:
+  "a * (a * b) = a * b"
+  by (simp add: assoc [symmetric])
+
+end
+
+locale lattice = inf!: abel_semigroup inf + sup!: abel_semigroup sup
+  for inf (infixl "\<sqinter>" 70) and sup (infixl "\<squnion>" 70) +
+  assumes sup_inf_absorb: "a \<squnion> (a \<sqinter> b) = a"
+  and inf_sup_absorb: "a \<sqinter> (a \<squnion> b) = a"
+
+sublocale lattice < inf!: semilattice inf
+proof
+  fix a
+  have "a \<sqinter> (a \<squnion> (a \<sqinter> a)) = a" by (fact inf_sup_absorb)
+  then show "a \<sqinter> a = a" by (simp add: sup_inf_absorb)
+qed
+
+sublocale lattice < sup!: semilattice sup
+proof
+  fix a
+  have "a \<squnion> (a \<sqinter> (a \<squnion> a)) = a" by (fact sup_inf_absorb)
+  then show "a \<squnion> a = a" by (simp add: inf_sup_absorb)
+qed
+
+
+subsection {* Generic algebraic operations *}
+
+class zero = 
+  fixes zero :: 'a  ("0")
+
+class one =
+  fixes one  :: 'a  ("1")
+
+lemma Let_0 [simp]: "Let 0 f = f 0"
+  unfolding Let_def ..
+
+lemma Let_1 [simp]: "Let 1 f = f 1"
+  unfolding Let_def ..
+
+setup {*
+  Reorient_Proc.add
+    (fn Const(@{const_name Algebras.zero}, _) => true
+      | Const(@{const_name Algebras.one}, _) => true
+      | _ => false)
+*}
+
+simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
+simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
+
+typed_print_translation {*
+let
+  fun tr' c = (c, fn show_sorts => fn T => fn ts =>
+    if (not o null) ts orelse T = dummyT
+      orelse not (! show_types) andalso can Term.dest_Type T
+    then raise Match
+    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
+in map tr' [@{const_syntax Algebras.one}, @{const_syntax Algebras.zero}] end;
+*} -- {* show types that are presumably too general *}
+
+hide (open) const zero one
+
+class plus =
+  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
+
+class minus =
+  fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
+
+class uminus =
+  fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
+
+class times =
+  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
+
+class inverse =
+  fixes inverse :: "'a \<Rightarrow> 'a"
+    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
+
+class abs =
+  fixes abs :: "'a \<Rightarrow> 'a"
+begin
+
+notation (xsymbols)
+  abs  ("\<bar>_\<bar>")
+
+notation (HTML output)
+  abs  ("\<bar>_\<bar>")
+
+end
+
+class sgn =
+  fixes sgn :: "'a \<Rightarrow> 'a"
+
+class ord =
+  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+begin
+
+notation
+  less_eq  ("op <=") and
+  less_eq  ("(_/ <= _)" [51, 51] 50) and
+  less  ("op <") and
+  less  ("(_/ < _)"  [51, 51] 50)
+  
+notation (xsymbols)
+  less_eq  ("op \<le>") and
+  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
+
+notation (HTML output)
+  less_eq  ("op \<le>") and
+  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
+
+abbreviation (input)
+  greater_eq  (infix ">=" 50) where
+  "x >= y \<equiv> y <= x"
+
+notation (input)
+  greater_eq  (infix "\<ge>" 50)
+
+abbreviation (input)
+  greater  (infix ">" 50) where
+  "x > y \<equiv> y < x"
+
+end
+
+syntax
+  "_index1"  :: index    ("\<^sub>1")
+translations
+  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
+
+end
\ No newline at end of file
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -655,7 +655,7 @@
     if h aconvc y then false else if h aconvc x then true else earlier t x y;
 
 fun dest_frac ct = case term_of ct of
-   Const (@{const_name "HOL.divide"},_) $ a $ b=>
+   Const (@{const_name Algebras.divide},_) $ a $ b=>
     Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
  | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
  | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
@@ -670,13 +670,13 @@
  end
 
 fun whatis x ct = case term_of ct of
-  Const(@{const_name "HOL.plus"}, _)$(Const(@{const_name "HOL.times"},_)$_$y)$_ =>
+  Const(@{const_name Algebras.plus}, _)$(Const(@{const_name Algebras.times},_)$_$y)$_ =>
      if y aconv term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct])
      else ("Nox",[])
-| Const(@{const_name "HOL.plus"}, _)$y$_ =>
+| Const(@{const_name Algebras.plus}, _)$y$_ =>
      if y aconv term_of x then ("x+t",[Thm.dest_arg ct])
      else ("Nox",[])
-| Const(@{const_name "HOL.times"}, _)$_$y =>
+| Const(@{const_name Algebras.times}, _)$_$y =>
      if y aconv term_of x then ("c*x",[Thm.dest_arg1 ct])
      else ("Nox",[])
 | t => if t aconv term_of x then ("x",[]) else ("Nox",[]);
@@ -684,7 +684,7 @@
 fun xnormalize_conv ctxt [] ct = reflexive ct
 | xnormalize_conv ctxt (vs as (x::_)) ct =
    case term_of ct of
-   Const(@{const_name HOL.less},_)$_$Const(@{const_name "HOL.zero"},_) =>
+   Const(@{const_name Algebras.less},_)$_$Const(@{const_name Algebras.zero},_) =>
     (case whatis x (Thm.dest_arg1 ct) of
     ("c*x+t",[c,t]) =>
        let
@@ -727,7 +727,7 @@
     | _ => reflexive ct)
 
 
-|  Const(@{const_name HOL.less_eq},_)$_$Const(@{const_name "HOL.zero"},_) =>
+|  Const(@{const_name Algebras.less_eq},_)$_$Const(@{const_name Algebras.zero},_) =>
    (case whatis x (Thm.dest_arg1 ct) of
     ("c*x+t",[c,t]) =>
        let
@@ -771,7 +771,7 @@
       in rth end
     | _ => reflexive ct)
 
-|  Const("op =",_)$_$Const(@{const_name "HOL.zero"},_) =>
+|  Const("op =",_)$_$Const(@{const_name Algebras.zero},_) =>
    (case whatis x (Thm.dest_arg1 ct) of
     ("c*x+t",[c,t]) =>
        let
@@ -816,7 +816,7 @@
   val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
 in
 fun field_isolate_conv phi ctxt vs ct = case term_of ct of
-  Const(@{const_name HOL.less},_)$a$b =>
+  Const(@{const_name Algebras.less},_)$a$b =>
    let val (ca,cb) = Thm.dest_binop ct
        val T = ctyp_of_term ca
        val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
@@ -825,7 +825,7 @@
               (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
        val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
-| Const(@{const_name HOL.less_eq},_)$a$b =>
+| Const(@{const_name Algebras.less_eq},_)$a$b =>
    let val (ca,cb) = Thm.dest_binop ct
        val T = ctyp_of_term ca
        val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
@@ -856,11 +856,11 @@
                             else Ferrante_Rackoff_Data.Nox
    | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
                             else Ferrante_Rackoff_Data.Nox
-   | Const(@{const_name HOL.less},_)$y$z =>
+   | Const(@{const_name Algebras.less},_)$y$z =>
        if term_of x aconv y then Ferrante_Rackoff_Data.Lt
         else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
         else Ferrante_Rackoff_Data.Nox
-   | Const (@{const_name HOL.less_eq},_)$y$z =>
+   | Const (@{const_name Algebras.less_eq},_)$y$z =>
          if term_of x aconv y then Ferrante_Rackoff_Data.Le
          else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
          else Ferrante_Rackoff_Data.Nox
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -2963,11 +2963,11 @@
 fun num rT x = HOLogic.mk_number rT x;
 fun rrelT rT = [rT,rT] ---> rT;
 fun rrT rT = [rT, rT] ---> bT;
-fun divt rT = Const(@{const_name "HOL.divide"},rrelT rT);
-fun timest rT = Const(@{const_name "HOL.times"},rrelT rT);
-fun plust rT = Const(@{const_name "HOL.plus"},rrelT rT);
-fun minust rT = Const(@{const_name "HOL.minus"},rrelT rT);
-fun uminust rT = Const(@{const_name "HOL.uminus"}, rT --> rT);
+fun divt rT = Const(@{const_name Algebras.divide},rrelT rT);
+fun timest rT = Const(@{const_name Algebras.times},rrelT rT);
+fun plust rT = Const(@{const_name Algebras.plus},rrelT rT);
+fun minust rT = Const(@{const_name Algebras.minus},rrelT rT);
+fun uminust rT = Const(@{const_name Algebras.uminus}, rT --> rT);
 fun powt rT = Const(@{const_name "power"}, [rT,@{typ "nat"}] ---> rT);
 val brT = [bT, bT] ---> bT;
 val nott = @{term "Not"};
@@ -2975,10 +2975,10 @@
 val disjt = @{term "op |"};
 val impt = @{term "op -->"};
 val ifft = @{term "op = :: bool => _"}
-fun llt rT = Const(@{const_name "HOL.less"},rrT rT);
-fun lle rT = Const(@{const_name "HOL.less"},rrT rT);
+fun llt rT = Const(@{const_name Algebras.less},rrT rT);
+fun lle rT = Const(@{const_name Algebras.less},rrT rT);
 fun eqt rT = Const("op =",rrT rT);
-fun rz rT = Const(@{const_name "HOL.zero"},rT);
+fun rz rT = Const(@{const_name Algebras.zero},rT);
 
 fun dest_nat t = case t of
   Const ("Suc",_)$t' => 1 + dest_nat t'
@@ -2986,21 +2986,21 @@
 
 fun num_of_term m t = 
  case t of
-   Const(@{const_name "uminus"},_)$t => FRPar.Neg (num_of_term m t)
- | Const(@{const_name "HOL.plus"},_)$a$b => FRPar.Add (num_of_term m a, num_of_term m b)
- | Const(@{const_name "HOL.minus"},_)$a$b => FRPar.Sub (num_of_term m a, num_of_term m b)
- | Const(@{const_name "HOL.times"},_)$a$b => FRPar.Mul (num_of_term m a, num_of_term m b)
- | Const(@{const_name "power"},_)$a$n => FRPar.Pw (num_of_term m a, dest_nat n)
- | Const(@{const_name "HOL.divide"},_)$a$b => FRPar.C (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
+   Const(@{const_name Algebras.uminus},_)$t => FRPar.Neg (num_of_term m t)
+ | Const(@{const_name Algebras.plus},_)$a$b => FRPar.Add (num_of_term m a, num_of_term m b)
+ | Const(@{const_name Algebras.minus},_)$a$b => FRPar.Sub (num_of_term m a, num_of_term m b)
+ | Const(@{const_name Algebras.times},_)$a$b => FRPar.Mul (num_of_term m a, num_of_term m b)
+ | Const(@{const_name Power.power},_)$a$n => FRPar.Pw (num_of_term m a, dest_nat n)
+ | Const(@{const_name Algebras.divide},_)$a$b => FRPar.C (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
  | _ => (FRPar.C (HOLogic.dest_number t |> snd,1) 
          handle TERM _ => FRPar.Bound (AList.lookup (op aconv) m t |> the));
 
 fun tm_of_term m m' t = 
  case t of
-   Const(@{const_name "uminus"},_)$t => FRPar.tm_Neg (tm_of_term m m' t)
- | Const(@{const_name "HOL.plus"},_)$a$b => FRPar.tm_Add (tm_of_term m m' a, tm_of_term m m' b)
- | Const(@{const_name "HOL.minus"},_)$a$b => FRPar.tm_Sub (tm_of_term m m' a, tm_of_term m m' b)
- | Const(@{const_name "HOL.times"},_)$a$b => FRPar.tm_Mul (num_of_term m' a, tm_of_term m m' b)
+   Const(@{const_name Algebras.uminus},_)$t => FRPar.tm_Neg (tm_of_term m m' t)
+ | Const(@{const_name Algebras.plus},_)$a$b => FRPar.tm_Add (tm_of_term m m' a, tm_of_term m m' b)
+ | Const(@{const_name Algebras.minus},_)$a$b => FRPar.tm_Sub (tm_of_term m m' a, tm_of_term m m' b)
+ | Const(@{const_name Algebras.times},_)$a$b => FRPar.tm_Mul (num_of_term m' a, tm_of_term m m' b)
  | _ => (FRPar.CP (num_of_term m' t) 
          handle TERM _ => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the)
               | Option => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the));
@@ -3040,9 +3040,9 @@
   | Const("op =",ty)$p$q => 
        if domain_type ty = bT then FRPar.Iff(fm_of_term m m' p, fm_of_term m m' q)
        else FRPar.Eq (FRPar.tm_Sub(tm_of_term m m' p, tm_of_term m m' q))
-  | Const(@{const_name "HOL.less"},_)$p$q => 
+  | Const(@{const_name Algebras.less},_)$p$q => 
         FRPar.Lt (FRPar.tm_Sub(tm_of_term m m' p, tm_of_term m m' q))
-  | Const(@{const_name "HOL.less_eq"},_)$p$q => 
+  | Const(@{const_name Algebras.less_eq},_)$p$q => 
         FRPar.Le (FRPar.tm_Sub(tm_of_term m m' p, tm_of_term m m' q))
   | Const("Ex",_)$Abs(xn,xT,p) => 
      let val (xn', p') =  variant_abs (xn,xT,p)
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Decision_Procs/commutative_ring_tac.ML
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -13,8 +13,8 @@
 struct
 
 (* Zero and One of the commutative ring *)
-fun cring_zero T = Const (@{const_name HOL.zero}, T);
-fun cring_one T = Const (@{const_name HOL.one}, T);
+fun cring_zero T = Const (@{const_name Algebras.zero}, T);
+fun cring_one T = Const (@{const_name Algebras.one}, T);
 
 (* reification functions *)
 (* add two polynom expressions *)
@@ -49,13 +49,13 @@
   | reif_pol T vs t = pol_Pc T $ t;
 
 (* reification of polynom expressions *)
-fun reif_polex T vs (Const (@{const_name HOL.plus}, _) $ a $ b) =
+fun reif_polex T vs (Const (@{const_name Algebras.plus}, _) $ a $ b) =
       polex_add T $ reif_polex T vs a $ reif_polex T vs b
-  | reif_polex T vs (Const (@{const_name HOL.minus}, _) $ a $ b) =
+  | reif_polex T vs (Const (@{const_name Algebras.minus}, _) $ a $ b) =
       polex_sub T $ reif_polex T vs a $ reif_polex T vs b
-  | reif_polex T vs (Const (@{const_name HOL.times}, _) $ a $ b) =
+  | reif_polex T vs (Const (@{const_name Algebras.times}, _) $ a $ b) =
       polex_mul T $ reif_polex T vs a $ reif_polex T vs b
-  | reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) =
+  | reif_polex T vs (Const (@{const_name Algebras.uminus}, _) $ a) =
       polex_neg T $ reif_polex T vs a
   | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
       polex_pow T $ reif_polex T vs a $ n
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Groebner_Basis.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -527,13 +527,13 @@
     val (l,r) = Thm.dest_binop ct
     val T = ctyp_of_term l
   in (case (term_of l, term_of r) of
-      (Const(@{const_name "HOL.divide"},_)$_$_, _) =>
+      (Const(@{const_name Algebras.divide},_)$_$_, _) =>
         let val (x,y) = Thm.dest_binop l val z = r
             val _ = map (HOLogic.dest_number o term_of) [x,y,z]
             val ynz = prove_nz ss T y
         in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
         end
-     | (_, Const (@{const_name "HOL.divide"},_)$_$_) =>
+     | (_, Const (@{const_name Algebras.divide},_)$_$_) =>
         let val (x,y) = Thm.dest_binop r val z = l
             val _ = map (HOLogic.dest_number o term_of) [x,y,z]
             val ynz = prove_nz ss T y
@@ -543,49 +543,49 @@
   end
   handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
 
- fun is_number (Const(@{const_name "HOL.divide"},_)$a$b) = is_number a andalso is_number b
+ fun is_number (Const(@{const_name Algebras.divide},_)$a$b) = is_number a andalso is_number b
    | is_number t = can HOLogic.dest_number t
 
  val is_number = is_number o term_of
 
  fun proc3 phi ss ct =
   (case term_of ct of
-    Const(@{const_name HOL.less},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
+    Const(@{const_name Algebras.less},_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
       let
         val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
         val _ = map is_number [a,b,c]
         val T = ctyp_of_term c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name HOL.less_eq},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
+  | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
       let
         val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
         val _ = map is_number [a,b,c]
         val T = ctyp_of_term c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
       in SOME (mk_meta_eq th) end
-  | Const("op =",_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
+  | Const("op =",_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
       let
         val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
         val _ = map is_number [a,b,c]
         val T = ctyp_of_term c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name HOL.less},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
+  | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
     let
       val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
         val _ = map is_number [a,b,c]
         val T = ctyp_of_term c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name HOL.less_eq},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
+  | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
     let
       val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
         val _ = map is_number [a,b,c]
         val T = ctyp_of_term c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
       in SOME (mk_meta_eq th) end
-  | Const("op =",_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
+  | Const("op =",_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
     let
       val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
         val _ = map is_number [a,b,c]
@@ -645,15 +645,15 @@
 
 fun numeral_is_const ct =
   case term_of ct of
-   Const (@{const_name "HOL.divide"},_) $ a $ b =>
+   Const (@{const_name Algebras.divide},_) $ a $ b =>
      can HOLogic.dest_number a andalso can HOLogic.dest_number b
- | Const (@{const_name "HOL.inverse"},_)$t => can HOLogic.dest_number t
+ | Const (@{const_name Algebras.inverse},_)$t => can HOLogic.dest_number t
  | t => can HOLogic.dest_number t
 
 fun dest_const ct = ((case term_of ct of
-   Const (@{const_name "HOL.divide"},_) $ a $ b=>
+   Const (@{const_name Algebras.divide},_) $ a $ b=>
     Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
- | Const (@{const_name "HOL.inverse"},_)$t => 
+ | Const (@{const_name Algebras.inverse},_)$t => 
                Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
  | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
    handle TERM _ => error "ring_dest_const")
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/HOL.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -1625,118 +1625,6 @@
 by blast+
 
 
-subsection {* Generic classes and algebraic operations *}
-
-class zero = 
-  fixes zero :: 'a  ("0")
-
-class one =
-  fixes one  :: 'a  ("1")
-
-lemma Let_0 [simp]: "Let 0 f = f 0"
-  unfolding Let_def ..
-
-lemma Let_1 [simp]: "Let 1 f = f 1"
-  unfolding Let_def ..
-
-setup {*
-  Reorient_Proc.add
-    (fn Const(@{const_name HOL.zero}, _) => true
-      | Const(@{const_name HOL.one}, _) => true
-      | _ => false)
-*}
-
-simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
-simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
-
-typed_print_translation {*
-let
-  fun tr' c = (c, fn show_sorts => fn T => fn ts =>
-    if (not o null) ts orelse T = dummyT
-      orelse not (! show_types) andalso can Term.dest_Type T
-    then raise Match
-    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
-in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end;
-*} -- {* show types that are presumably too general *}
-
-hide (open) const zero one
-
-class plus =
-  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
-
-class minus =
-  fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
-
-class uminus =
-  fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
-
-class times =
-  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
-
-class inverse =
-  fixes inverse :: "'a \<Rightarrow> 'a"
-    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
-
-class abs =
-  fixes abs :: "'a \<Rightarrow> 'a"
-begin
-
-notation (xsymbols)
-  abs  ("\<bar>_\<bar>")
-
-notation (HTML output)
-  abs  ("\<bar>_\<bar>")
-
-end
-
-class sgn =
-  fixes sgn :: "'a \<Rightarrow> 'a"
-
-class ord =
-  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-begin
-
-notation
-  less_eq  ("op <=") and
-  less_eq  ("(_/ <= _)" [51, 51] 50) and
-  less  ("op <") and
-  less  ("(_/ < _)"  [51, 51] 50)
-  
-notation (xsymbols)
-  less_eq  ("op \<le>") and
-  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
-
-notation (HTML output)
-  less_eq  ("op \<le>") and
-  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
-
-abbreviation (input)
-  greater_eq  (infix ">=" 50) where
-  "x >= y \<equiv> y <= x"
-
-notation (input)
-  greater_eq  (infix "\<ge>" 50)
-
-abbreviation (input)
-  greater  (infix ">" 50) where
-  "x > y \<equiv> y < x"
-
-end
-
-syntax
-  "_index1"  :: index    ("\<^sub>1")
-translations
-  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
-
-lemma mk_left_commute:
-  fixes f (infix "\<otimes>" 60)
-  assumes a: "\<And>x y z. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" and
-          c: "\<And>x y. x \<otimes> y = y \<otimes> x"
-  shows "x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
-  by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]])
-
-
 subsection {* Basic ML bindings *}
 
 ML {*
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -58,7 +58,7 @@
   let val T as Type ("fun",[t,_]) = fastype_of trm
   in Collect_const t $ trm end;
 
-fun inclt ty = Const (@{const_name HOL.less_eq}, [ty,ty] ---> boolT);
+fun inclt ty = Const (@{const_name Algebras.less_eq}, [ty,ty] ---> boolT);
 
 
 fun Mset ctxt prop =
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -166,7 +166,7 @@
 import_theory prim_rec;
 
 const_maps
-    "<" > HOL.ord_class.less :: "[nat,nat]=>bool";
+    "<" > Algebras.less :: "[nat,nat]=>bool";
 
 end_import;
 
@@ -181,15 +181,15 @@
   ">"          > HOL4Compat.nat_gt
   ">="         > HOL4Compat.nat_ge
   FUNPOW       > HOL4Compat.FUNPOW
-  "<="         > HOL.ord_class.less_eq :: "[nat,nat]=>bool"
-  "+"          > HOL.plus_class.plus       :: "[nat,nat]=>nat"
-  "*"          > HOL.times_class.times      :: "[nat,nat]=>nat"
-  "-"          > HOL.minus_class.minus      :: "[nat,nat]=>nat"
-  MIN          > Orderings.ord_class.min    :: "[nat,nat]=>nat"
-  MAX          > Orderings.ord_class.max    :: "[nat,nat]=>nat"
-  DIV          > Divides.div_class.div :: "[nat,nat]=>nat"
-  MOD          > Divides.div_class.mod :: "[nat,nat]=>nat"
-  EXP          > Power.power_class.power :: "[nat,nat]=>nat";
+  "<="         > Algebras.less_eq :: "[nat,nat]=>bool"
+  "+"          > Algebras.plus :: "[nat,nat]=>nat"
+  "*"          > Algebras.times :: "[nat,nat]=>nat"
+  "-"          > Algebras.minus :: "[nat,nat]=>nat"
+  MIN          > Orderings.min :: "[nat,nat]=>nat"
+  MAX          > Orderings.max :: "[nat,nat]=>nat"
+  DIV          > Divides.div :: "[nat,nat]=>nat"
+  MOD          > Divides.mod :: "[nat,nat]=>nat"
+  EXP          > Power.power :: "[nat,nat]=>nat";
 
 end_import;
 
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Import/Generate-HOL/GenHOL4Real.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Import/Generate-HOL/GenHOL4Real.thy
-    ID:         $Id$
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
@@ -17,13 +16,13 @@
   real > RealDef.real;
 
 const_maps
-  real_0   > 0           :: real
-  real_1   > 1           :: real
-  real_neg > uminus      :: "real => real"
-  inv      > HOL.inverse :: "real => real"
-  real_add > HOL.plus    :: "[real,real] => real"
-  real_mul > HOL.times   :: "[real,real] => real"
-  real_lt  > HOL.ord_class.less :: "[real,real] => bool";
+  real_0   > Algebras.zero      :: real
+  real_1   > Algebras.one       :: real
+  real_neg > Algebras.uminus    :: "real => real"
+  inv      > Algebras.inverse   :: "real => real"
+  real_add > Algebras.plus      :: "[real,real] => real"
+  real_mul > Algebras.times     :: "[real,real] => real"
+  real_lt  > Algebras.less      :: "[real,real] => bool";
 
 ignore_thms
     real_TY_DEF
@@ -51,11 +50,11 @@
 const_maps
   real_gt     > HOL4Compat.real_gt
   real_ge     > HOL4Compat.real_ge
-  real_lte    > HOL.ord_class.less_eq :: "[real,real] => bool"
-  real_sub    > HOL.minus    :: "[real,real] => real"
-  "/"         > HOL.divide   :: "[real,real] => real"
-  pow         > Power.power_class.power    :: "[real,nat] => real"
-  abs         > HOL.abs      :: "real => real"
+  real_lte    > Algebras.less_eq :: "[real,real] => bool"
+  real_sub    > Algebras.minus :: "[real,real] => real"
+  "/"         > Algebras.divide :: "[real,real] => real"
+  pow         > Power.power :: "[real,nat] => real"
+  abs         > Algebras.abs :: "real => real"
   real_of_num > RealDef.real :: "nat => real";
 
 end_import;
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -76,9 +76,9 @@
   SUC > Suc
   PRE > HOLLightCompat.Pred
   NUMERAL > HOL4Compat.NUMERAL
-  "+" > HOL.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
-  "*" > HOL.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  "-" > HOL.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  "+" > Algebras.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
+  "*" > Algebras.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  "-" > Algebras.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   BIT0 > HOLLightCompat.NUMERAL_BIT0
   BIT1 > HOL4Compat.NUMERAL_BIT1
   INL > Sum_Type.Inl
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Import/HOL/arithmetic.imp
--- a/src/HOL/Import/HOL/arithmetic.imp	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/HOL/arithmetic.imp	Thu Jan 28 11:48:49 2010 +0100
@@ -23,10 +23,10 @@
   "ALT_ZERO" > "HOL4Compat.ALT_ZERO"
   ">=" > "HOL4Compat.nat_ge"
   ">" > "HOL4Compat.nat_gt"
-  "<=" > "HOL.ord_class.less_eq" :: "nat => nat => bool"
-  "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
-  "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
-  "*" > "HOL.times_class.times" :: "nat => nat => nat"
+  "<=" > "Algebras.ord_class.less_eq" :: "nat => nat => bool"
+  "-" > "Algebras.minus_class.minus" :: "nat => nat => nat"
+  "+" > "Algebras.plus_class.plus" :: "nat => nat => nat"
+  "*" > "Algebras.times_class.times" :: "nat => nat => nat"
 
 thm_maps
   "num_case_def" > "HOL4Compat.num_case_def"
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Import/HOL/prim_rec.imp
--- a/src/HOL/Import/HOL/prim_rec.imp	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/HOL/prim_rec.imp	Thu Jan 28 11:48:49 2010 +0100
@@ -18,7 +18,7 @@
   "PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN"
   "PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC"
   "PRE" > "HOL4Base.prim_rec.PRE"
-  "<" > "HOL.ord_class.less" :: "nat => nat => bool"
+  "<" > "Algebras.less" :: "nat => nat => bool"
 
 thm_maps
   "wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef"
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Import/HOL/real.imp
--- a/src/HOL/Import/HOL/real.imp	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/HOL/real.imp	Thu Jan 28 11:48:49 2010 +0100
@@ -10,14 +10,14 @@
 const_maps
   "sup" > "HOL4Real.real.sup"
   "sum" > "HOL4Real.real.sum"
-  "real_sub" > "HOL.minus_class.minus" :: "real => real => real"
+  "real_sub" > "Algebras.minus" :: "real => real => real"
   "real_of_num" > "RealDef.real" :: "nat => real"
-  "real_lte" > "HOL.ord_class.less_eq" :: "real => real => bool"
+  "real_lte" > "Algebras.less_eq" :: "real => real => bool"
   "real_gt" > "HOL4Compat.real_gt"
   "real_ge" > "HOL4Compat.real_ge"
   "pow" > "Power.power_class.power" :: "real => nat => real"
-  "abs" > "HOL.minus_class.abs" :: "real => real"
-  "/" > "HOL.divides_class.divide" :: "real => real => real"
+  "abs" > "Algebras.abs" :: "real => real"
+  "/" > "Algebras.divide" :: "real => real => real"
 
 thm_maps
   "sup_def" > "HOL4Real.real.sup_def"
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Import/HOL/realax.imp
--- a/src/HOL/Import/HOL/realax.imp	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/HOL/realax.imp	Thu Jan 28 11:48:49 2010 +0100
@@ -27,13 +27,13 @@
   "treal_add" > "HOL4Real.realax.treal_add"
   "treal_1" > "HOL4Real.realax.treal_1"
   "treal_0" > "HOL4Real.realax.treal_0"
-  "real_neg" > "HOL.uminus_class.uminus" :: "real => real"
-  "real_mul" > "HOL.times_class.times" :: "real => real => real"
-  "real_lt" > "HOL.ord_class.less" :: "real => real => bool"
-  "real_add" > "HOL.plus_class.plus" :: "real => real => real"
-  "real_1" > "HOL.one_class.one" :: "real"
-  "real_0" > "HOL.zero_class.zero" :: "real"
-  "inv" > "HOL.divide_class.inverse" :: "real => real"
+  "real_neg" > "Algebras.uminus_class.uminus" :: "real => real"
+  "real_mul" > "Algebras.times_class.times" :: "real => real => real"
+  "real_lt" > "Algebras.ord_class.less" :: "real => real => bool"
+  "real_add" > "Algebras.plus_class.plus" :: "real => real => real"
+  "real_1" > "Algebras.one_class.one" :: "real"
+  "real_0" > "Algebras.zero_class.zero" :: "real"
+  "inv" > "Algebras.divide_class.inverse" :: "real => real"
   "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal"
 
 thm_maps
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Import/HOLLight/HOLLight.thy
--- a/src/HOL/Import/HOLLight/HOLLight.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/HOLLight/HOLLight.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -1119,37 +1119,37 @@
    (%x::nat.
        (All::(nat => bool) => bool)
         (%xa::nat.
-            (op =::nat => nat => bool) ((HOL.plus::nat => nat => nat) x xa)
-             ((HOL.plus::nat => nat => nat) x xa))))
+            (op =::nat => nat => bool) ((plus::nat => nat => nat) x xa)
+             ((plus::nat => nat => nat) x xa))))
  ((op &::bool => bool => bool)
-   ((op =::nat => nat => bool) ((HOL.plus::nat => nat => nat) (0::nat) (0::nat))
+   ((op =::nat => nat => bool) ((plus::nat => nat => nat) (0::nat) (0::nat))
      (0::nat))
    ((op &::bool => bool => bool)
      ((All::(nat => bool) => bool)
        (%x::nat.
            (op =::nat => nat => bool)
-            ((HOL.plus::nat => nat => nat) (0::nat)
+            ((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)
-              ((HOL.plus::nat => nat => nat) (0::nat)
+              ((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)
-                ((HOL.plus::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
+                ((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)
-                  ((HOL.plus::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
+                  ((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)
-                         ((HOL.plus::nat => nat => nat)
+                         ((plus::nat => nat => nat)
                            ((NUMERAL_BIT0::nat => nat) x)
                            ((NUMERAL_BIT0::nat => nat) xa))
                          ((NUMERAL_BIT0::nat => nat)
-                           ((HOL.plus::nat => nat => nat) x xa)))))
+                           ((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)
-                           ((HOL.plus::nat => nat => nat)
+                           ((plus::nat => nat => nat)
                              ((NUMERAL_BIT0::nat => nat) x)
                              ((NUMERAL_BIT1::nat => nat) xa))
                            ((NUMERAL_BIT1::nat => nat)
-                             ((HOL.plus::nat => nat => nat) x xa)))))
+                             ((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)
-                             ((HOL.plus::nat => nat => nat)
+                             ((plus::nat => nat => nat)
                                ((NUMERAL_BIT1::nat => nat) x)
                                ((NUMERAL_BIT0::nat => nat) xa))
                              ((NUMERAL_BIT1::nat => nat)
-                               ((HOL.plus::nat => nat => nat) x xa)))))
+                               ((plus::nat => nat => nat) x xa)))))
                  ((All::(nat => bool) => bool)
                    (%x::nat.
                        (All::(nat => bool) => bool)
                         (%xa::nat.
                             (op =::nat => nat => bool)
-                             ((HOL.plus::nat => nat => nat)
+                             ((plus::nat => nat => nat)
                                ((NUMERAL_BIT1::nat => nat) x)
                                ((NUMERAL_BIT1::nat => nat) xa))
                              ((NUMERAL_BIT0::nat => nat)
                                ((Suc::nat => nat)
-                                 ((HOL.plus::nat => nat => nat) x
+                                 ((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))
-                           ((HOL.plus::nat => nat => nat)
+                           ((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))
-                             ((HOL.plus::nat => nat => nat)
+                             ((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))
-                             ((HOL.plus::nat => nat => nat)
+                             ((plus::nat => nat => nat)
                                ((NUMERAL_BIT1::nat => nat) x)
-                               ((HOL.plus::nat => nat => nat)
+                               ((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 ((HOL.plus::nat => nat => nat) i
+           u ((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 ((HOL.plus::nat => nat => nat) i
+           u ((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)
- ((HOL.plus::nat => nat => nat)
+ ((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))
- ((HOL.plus::nat => nat => nat)
+ ((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)
-   (HOL.plus::nat => nat => nat))"
+   (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)
-   (HOL.plus::nat => nat => nat))"
+   (plus::nat => nat => nat))"
   by (import hollight DEF_nsum)
 
 lemma NEUTRAL_ADD: "(op =::nat => nat => bool)
- ((neutral::(nat => nat => nat) => nat) (HOL.plus::nat => nat => nat)) (0::nat)"
+ ((neutral::(nat => nat => nat) => nat) (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) (HOL.plus::nat => nat => nat)"
+lemma MONOIDAL_ADD: "(monoidal::(nat => nat => nat) => bool) (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 HOL.plus x xa) --> nsum (support HOL.plus x xa) x = nsum xa x"
+   FINITE (support plus x xa) --> nsum (support 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 ae634fad947e -r 18b41bba42b5 src/HOL/Import/HOLLight/hollight.imp
--- a/src/HOL/Import/HOLLight/hollight.imp	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/HOLLight/hollight.imp	Thu Jan 28 11:48:49 2010 +0100
@@ -238,10 +238,10 @@
   "<=" > "HOLLight.hollight.<="
   "<" > "HOLLight.hollight.<"
   "/\\" > "op &"
-  "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
+  "-" > "Algebras.minus_class.minus" :: "nat => nat => nat"
   "," > "Pair"
-  "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
-  "*" > "HOL.times_class.times" :: "nat => nat => nat"
+  "+" > "Algebras.plus_class.plus" :: "nat => nat => nat"
+  "*" > "Algebras.times_class.times" :: "nat => nat => nat"
   "$" > "HOLLight.hollight.$"
   "!" > "All"
 
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/IsaMakefile	Thu Jan 28 11:48:49 2010 +0100
@@ -141,6 +141,7 @@
 	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
 
 PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
+  Algebras.thy \
   Complete_Lattice.thy \
   Datatype.thy \
   Extraction.thy \
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Mutabelle/Mutabelle.thy
--- a/src/HOL/Mutabelle/Mutabelle.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Mutabelle/Mutabelle.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -7,16 +7,16 @@
 val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}];
 
 val forbidden =
- [(@{const_name "power"}, "'a"),
-  ("HOL.induct_equal", "'a"),
-  ("HOL.induct_implies", "'a"),
-  ("HOL.induct_conj", "'a"),
-  (@{const_name "undefined"}, "'a"),
-  (@{const_name "default"}, "'a"),
-  (@{const_name "dummy_pattern"}, "'a::{}"),
-  (@{const_name "uminus"}, "'a"),
-  (@{const_name "Nat.size"}, "'a"),
-  (@{const_name "HOL.abs"}, "'a")];
+ [(@{const_name Power.power}, "'a"),
+  (@{const_name HOL.induct_equal}, "'a"),
+  (@{const_name HOL.induct_implies}, "'a"),
+  (@{const_name HOL.induct_conj}, "'a"),
+  (@{const_name HOL.undefined}, "'a"),
+  (@{const_name HOL.default}, "'a"),
+  (@{const_name dummy_pattern}, "'a::{}"),
+  (@{const_name Algebras.uminus}, "'a"),
+  (@{const_name Nat.size}, "'a"),
+  (@{const_name Algebras.abs}, "'a")];
 
 val forbidden_thms =
  ["finite_intvl_succ_class",
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -189,15 +189,15 @@
 
 val forbidden =
  [(* (@{const_name "power"}, "'a"), *)
-  ("HOL.induct_equal", "'a"),
-  ("HOL.induct_implies", "'a"),
-  ("HOL.induct_conj", "'a"),
+  (@{const_name HOL.induct_equal}, "'a"),
+  (@{const_name HOL.induct_implies}, "'a"),
+  (@{const_name HOL.induct_conj}, "'a"),
   (@{const_name "undefined"}, "'a"),
   (@{const_name "default"}, "'a"),
   (@{const_name "dummy_pattern"}, "'a::{}") (*,
   (@{const_name "uminus"}, "'a"),
   (@{const_name "Nat.size"}, "'a"),
-  (@{const_name "HOL.abs"}, "'a") *)]
+  (@{const_name "Algebras.abs"}, "'a") *)]
 
 val forbidden_thms =
  ["finite_intvl_succ_class",
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/NSA/NSA.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -671,12 +671,12 @@
   0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
 fun reorient_proc sg _ (_ $ t $ u) =
   case u of
-      Const(@{const_name HOL.zero}, _) => NONE
-    | Const(@{const_name HOL.one}, _) => NONE
+      Const(@{const_name Algebras.zero}, _) => NONE
+    | Const(@{const_name Algebras.one}, _) => NONE
     | Const(@{const_name Int.number_of}, _) $ _ => NONE
     | _ => SOME (case t of
-                Const(@{const_name HOL.zero}, _) => meta_zero_approx_reorient
-              | Const(@{const_name HOL.one}, _) => meta_one_approx_reorient
+                Const(@{const_name Algebras.zero}, _) => meta_zero_approx_reorient
+              | Const(@{const_name Algebras.one}, _) => meta_one_approx_reorient
               | Const(@{const_name Int.number_of}, _) $ _ =>
                                  meta_number_of_approx_reorient);
 
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Orderings.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -5,7 +5,7 @@
 header {* Abstract orderings *}
 
 theory Orderings
-imports HOL
+imports Algebras
 uses
   "~~/src/Provers/order.ML"
   "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Prolog/Func.thy
--- a/src/HOL/Prolog/Func.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Prolog/Func.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -1,12 +1,11 @@
 (*  Title:    HOL/Prolog/Func.thy
-    ID:       $Id$
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
 *)
 
 header {* Untyped functional language, with call by value semantics *}
 
 theory Func
-imports HOHH
+imports HOHH Algebras
 begin
 
 typedecl tm
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Prolog/HOHH.thy
--- a/src/HOL/Prolog/HOHH.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Prolog/HOHH.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:    HOL/Prolog/HOHH.thy
-    ID:       $Id$
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
 *)
 
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Prolog/Test.thy
--- a/src/HOL/Prolog/Test.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Prolog/Test.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:    HOL/Prolog/Test.thy
-    ID:       $Id$
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
 *)
 
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Prolog/Type.thy
--- a/src/HOL/Prolog/Type.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Prolog/Type.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:    HOL/Prolog/Type.thy
-    ID:       $Id$
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
 *)
 
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Set.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -928,7 +928,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.
-  [("HOL.uminus", Compl_iff RS iffD1), ("HOL.minus", [Diff_iff RS iffD1]),
+  [("uminus", Compl_iff RS iffD1), ("minus", [Diff_iff RS iffD1]),
    ("Int", [IntD1,IntD2]),
    ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
  *)
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -80,10 +80,10 @@
   let
     val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
   in
-    case try_proof (goals @{const_name HOL.less}) solve_tac of
+    case try_proof (goals @{const_name Algebras.less}) solve_tac of
       Solved thm => Less thm
     | Stuck thm =>
-      (case try_proof (goals @{const_name HOL.less_eq}) solve_tac of
+      (case try_proof (goals @{const_name Algebras.less_eq}) solve_tac of
          Solved thm2 => LessEq (thm2, thm)
        | Stuck thm2 =>
          if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -25,7 +25,7 @@
 
 val lookup_size = SizeData.get #> Symtab.lookup;
 
-fun plus (t1, t2) = Const ("HOL.plus_class.plus",
+fun plus (t1, t2) = Const (@{const_name Algebras.plus},
   HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
 
 fun size_of_type f g h (T as Type (s, Ts)) =
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Function/termination.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -203,10 +203,10 @@
              HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
                $ (m2 $ r) $ (m1 $ l)))))) tac
   in
-    case try @{const_name HOL.less} of
+    case try @{const_name Algebras.less} of
        Solved thm => Less thm
      | Stuck thm =>
-       (case try @{const_name HOL.less_eq} of
+       (case try @{const_name Algebras.less_eq} of
           Solved thm2 => LessEq (thm2, thm)
         | Stuck thm2 =>
           if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -74,7 +74,7 @@
     Const (atom_name "" T j, T)
 
 (* term -> real *)
-fun extract_real_number (Const (@{const_name HOL.divide}, _) $ t1 $ t2) =
+fun extract_real_number (Const (@{const_name Algebras.divide}, _) $ t1 $ t2) =
     real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
   | extract_real_number t = real (snd (HOLogic.dest_number t))
 (* term * term -> order *)
@@ -434,7 +434,7 @@
                            0 => mk_num 0
                          | n1 => case HOLogic.dest_number t2 |> snd of
                                    1 => mk_num n1
-                                 | n2 => Const (@{const_name HOL.divide},
+                                 | n2 => Const (@{const_name Algebras.divide},
                                                 num_T --> num_T --> num_T)
                                          $ mk_num n1 $ mk_num n2)
                       | _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -1561,7 +1561,7 @@
   end;
 
 (* special setup for simpset *)                  
-val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms "HOL.simp_thms"} @ [@{thm Pair_eq}])
+val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms HOL.simp_thms} @ [@{thm Pair_eq}])
   setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
   setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
 
@@ -1817,7 +1817,7 @@
      (* make this simpset better! *)
     asm_full_simp_tac (HOL_basic_ss' addsimps simprules) 1
     THEN print_tac' options "after prove_match:"
-    THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm "HOL.if_P"}] 1
+    THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm HOL.if_P}] 1
            THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1))))
            THEN print_tac' options "if condition to be solved:"
            THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1 THEN print_tac' options "after if simp; in SOLVED:"))
@@ -1843,7 +1843,7 @@
   in 
     (* remove not_False_eq_True when simpset in prove_match is better *)
     simp_tac (HOL_basic_ss addsimps
-      (@{thms "HOL.simp_thms"} @ (@{thm not_False_eq_True} :: @{thm eval_pred} :: defs))) 1 
+      (@{thms HOL.simp_thms} @ (@{thm not_False_eq_True} :: @{thm eval_pred} :: defs))) 1 
     (* need better control here! *)
   end
 
@@ -2435,8 +2435,8 @@
       val [polarity, depth] = additional_arguments
       val polarity' = (case prem of Prem _ => I | Negprem _ => HOLogic.mk_not | _ => I) polarity
       val depth' =
-        Const ("HOL.minus_class.minus", @{typ "code_numeral => code_numeral => code_numeral"})
-          $ depth $ Const ("HOL.one_class.one", @{typ "Code_Numeral.code_numeral"})
+        Const ("Algebras.minus", @{typ "code_numeral => code_numeral => code_numeral"})
+          $ depth $ Const ("Algebras.one", @{typ "Code_Numeral.code_numeral"})
     in [polarity', depth'] end
   }
 
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -219,21 +219,21 @@
    @{const_name "op &"}]
 
 fun special_cases (c, T) = member (op =) [
-  @{const_name "Product_Type.Unity"},
-  @{const_name "False"},
-  @{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat},
+  @{const_name Product_Type.Unity},
+  @{const_name False},
+  @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
   @{const_name Nat.one_nat_inst.one_nat},
-  @{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"},
-  @{const_name "HOL.zero_class.zero"},
-  @{const_name "HOL.one_class.one"},  @{const_name HOL.plus_class.plus},
+  @{const_name Algebras.ord_class.less}, @{const_name Algebras.ord_class.less_eq},
+  @{const_name Algebras.zero},
+  @{const_name Algebras.one},  @{const_name Algebras.plus},
   @{const_name Nat.ord_nat_inst.less_eq_nat},
   @{const_name Nat.ord_nat_inst.less_nat},
   @{const_name number_nat_inst.number_of_nat},
   @{const_name Int.Bit0},
   @{const_name Int.Bit1},
   @{const_name Int.Pls},
-  @{const_name "Int.zero_int_inst.zero_int"},
-  @{const_name "List.filter"}] c
+  @{const_name Int.zero_int_inst.zero_int},
+  @{const_name List.filter}] c
 
 fun print_specification options thy constname specs = 
   if show_intermediate_results options then
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -73,15 +73,15 @@
 | Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
 | Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) =>
   if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
-| Const (@{const_name HOL.less}, _) $ y$ z =>
+| Const (@{const_name Algebras.less}, _) $ y$ z =>
    if term_of x aconv y then Lt (Thm.dest_arg ct)
    else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
-| Const (@{const_name HOL.less_eq}, _) $ y $ z =>
+| Const (@{const_name Algebras.less_eq}, _) $ y $ z =>
    if term_of x aconv y then Le (Thm.dest_arg ct)
    else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
-| Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_) =>
+| Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_) =>
    if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
-| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_)) =>
+| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_)) =>
    if term_of x aconv y then
    NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
 | _ => Nox)
@@ -175,18 +175,18 @@
   (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]);
 fun linear_cmul 0 tm = zero
   | linear_cmul n tm = case tm of
-      Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
-    | Const (@{const_name HOL.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
-    | Const (@{const_name HOL.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
-    | (m as Const (@{const_name HOL.uminus}, _)) $ a => m $ linear_cmul n a
+      Const (@{const_name Algebras.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
+    | Const (@{const_name Algebras.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
+    | Const (@{const_name Algebras.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
+    | (m as Const (@{const_name Algebras.uminus}, _)) $ a => m $ linear_cmul n a
     | _ => numeral1 (fn m => n * m) tm;
 fun earlier [] x y = false
   | earlier (h::t) x y =
     if h aconv y then false else if h aconv x then true else earlier t x y;
 
 fun linear_add vars tm1 tm2 = case (tm1, tm2) of
-    (Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1,
-    Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) =>
+    (Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c1 $ x1) $ r1,
+    Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c2 $ x2) $ r2) =>
    if x1 = x2 then
      let val c = numeral2 Integer.add c1 c2
       in if c = zero then linear_add vars r1 r2
@@ -194,9 +194,9 @@
      end
      else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
    else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
- | (Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1, _) =>
+ | (Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c1 $ x1) $ r1, _) =>
       addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
- | (_, Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) =>
+ | (_, Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c2 $ x2) $ r2) =>
       addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
  | (_, _) => numeral2 Integer.add tm1 tm2;
 
@@ -205,10 +205,10 @@
 
 
 fun lint vars tm =  if is_numeral tm then tm  else case tm of
-  Const (@{const_name HOL.uminus}, _) $ t => linear_neg (lint vars t)
-| Const (@{const_name HOL.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
-| Const (@{const_name HOL.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
-| Const (@{const_name HOL.times}, _) $ s $ t =>
+  Const (@{const_name Algebras.uminus}, _) $ t => linear_neg (lint vars t)
+| Const (@{const_name Algebras.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
+| Const (@{const_name Algebras.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
+| Const (@{const_name Algebras.times}, _) $ s $ t =>
   let val s' = lint vars s
       val t' = lint vars t
   in if is_numeral s' then (linear_cmul (dest_numeral s') t')
@@ -217,10 +217,10 @@
   end
  | _ => addC $ (mulC $ one $ tm) $ zero;
 
-fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.less}, T) $ s $ t)) =
-    lin vs (Const (@{const_name HOL.less_eq}, T) $ t $ s)
-  | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) =
-    lin vs (Const (@{const_name HOL.less}, T) $ t $ s)
+fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Algebras.less}, T) $ s $ t)) =
+    lin vs (Const (@{const_name Algebras.less_eq}, T) $ t $ s)
+  | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Algebras.less_eq}, T) $ s $ t)) =
+    lin vs (Const (@{const_name Algebras.less}, T) $ t $ s)
   | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
   | lin (vs as x::_) (Const(@{const_name Ring_and_Field.dvd},_)$d$t) =
     HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} (numeral1 abs d, lint vs t)
@@ -270,7 +270,7 @@
       val d'' = Thm.rhs_of dth |> Thm.dest_arg1
      in
       case tt' of
-        Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$_)$_ =>
+        Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$_)$_ =>
         let val x = dest_numeral c
         in if x < 0 then Conv.fconv_rule (arg_conv (arg_conv (lint_conv ctxt vs)))
                                        (Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
@@ -293,15 +293,15 @@
   val ins = insert (op = : int * int -> bool)
   fun h (acc,dacc) t =
    case (term_of t) of
-    Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ =>
+    Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ =>
     if x aconv y andalso member (op =)
-      ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
+      ["op =", @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
     then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
-  | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) =>
+  | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
     if x aconv y andalso member (op =)
-       [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
+       [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
     then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
-  | Const(@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_) =>
+  | Const(@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_) =>
     if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
   | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
@@ -335,15 +335,15 @@
    Const("op &",_)$_$_ => binop_conv unit_conv t
   | Const("op |",_)$_$_ => binop_conv unit_conv t
   | Const (@{const_name Not},_)$_ => arg_conv unit_conv t
-  | Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ =>
+  | Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ =>
     if x=y andalso member (op =)
-      ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
+      ["op =", @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
     then cv (l div dest_numeral c) t else Thm.reflexive t
-  | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) =>
+  | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
     if x=y andalso member (op =)
-      [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
+      [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
     then cv (l div dest_numeral c) t else Thm.reflexive t
-  | Const(@{const_name Ring_and_Field.dvd},_)$d$(r as (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_)) =>
+  | Const(@{const_name Ring_and_Field.dvd},_)$d$(r as (Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_)) =>
     if x=y then
       let
        val k = l div dest_numeral c
@@ -546,10 +546,10 @@
   | @{term "0::int"} => C 0
   | @{term "1::int"} => C 1
   | Term.Bound i => Bound i
-  | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t')
-  | Const(@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
-  | Const(@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
-  | Const(@{const_name HOL.times},_)$t1$t2 =>
+  | Const(@{const_name Algebras.uminus},_)$t' => Neg (i_of_term vs t')
+  | Const(@{const_name Algebras.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
+  | Const(@{const_name Algebras.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
+  | Const(@{const_name Algebras.times},_)$t1$t2 =>
      (Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
     handle TERM _ =>
        (Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
@@ -560,8 +560,8 @@
 fun qf_of_term ps vs t =  case t
  of Const("True",_) => T
   | Const("False",_) => F
-  | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
-  | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
+  | Const(@{const_name Algebras.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
+  | Const(@{const_name Algebras.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
   | Const(@{const_name Ring_and_Field.dvd},_)$t1$t2 =>
       (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")  (* FIXME avoid handle _ *)
   | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/Qelim/cooper_data.ML
--- a/src/HOL/Tools/Qelim/cooper_data.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -33,7 +33,7 @@
    @{term "abs :: int => _"},
    @{term "max :: int => _"}, @{term "max :: nat => _"},
    @{term "min :: int => _"}, @{term "min :: nat => _"},
-   @{term "HOL.uminus :: int => _"}, (*@ {term "HOL.uminus :: nat => _"},*)
+   @{term "uminus :: int => _"}, (*@ {term "uminus :: nat => _"},*)
    @{term "Not"}, @{term "Suc"},
    @{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
    @{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -52,15 +52,15 @@
 
 local
  fun isnum t = case t of 
-   Const(@{const_name HOL.zero},_) => true
- | Const(@{const_name HOL.one},_) => true
+   Const(@{const_name Algebras.zero},_) => true
+ | Const(@{const_name Algebras.one},_) => true
  | @{term "Suc"}$s => isnum s
  | @{term "nat"}$s => isnum s
  | @{term "int"}$s => isnum s
- | Const(@{const_name HOL.uminus},_)$s => isnum s
- | Const(@{const_name HOL.plus},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name HOL.times},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name HOL.minus},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Algebras.uminus},_)$s => isnum s
+ | Const(@{const_name Algebras.plus},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Algebras.times},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Algebras.minus},_)$l$r => isnum l andalso isnum r
  | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
  | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
  | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/arith_data.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -75,11 +75,11 @@
 
 fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n;
 
-val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
+val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus};
 
 fun mk_minus t = 
   let val T = Term.fastype_of t
-  in Const (@{const_name HOL.uminus}, T --> T) $ t end;
+  in Const (@{const_name Algebras.uminus}, T --> T) $ t end;
 
 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
 fun mk_sum T []        = mk_number T 0
@@ -91,9 +91,9 @@
   | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
 
 (*decompose additions AND subtractions as a sum*)
-fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) =
+fun dest_summing (pos, Const (@{const_name Algebras.plus}, _) $ t $ u, ts) =
         dest_summing (pos, t, dest_summing (pos, u, ts))
-  | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) =
+  | dest_summing (pos, Const (@{const_name Algebras.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;
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/hologic.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -440,9 +440,9 @@
 
 val natT = Type ("nat", []);
 
-val zero = Const ("HOL.zero_class.zero", natT);
+val zero = Const ("Algebras.zero_class.zero", natT);
 
-fun is_zero (Const ("HOL.zero_class.zero", _)) = true
+fun is_zero (Const ("Algebras.zero_class.zero", _)) = true
   | is_zero _ = false;
 
 fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
@@ -458,7 +458,7 @@
       | mk n = mk_Suc (mk (n - 1));
   in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end;
 
-fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0
+fun dest_nat (Const ("Algebras.zero_class.zero", _)) = 0
   | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
   | dest_nat t = raise TERM ("dest_nat", [t]);
 
@@ -508,12 +508,12 @@
   | add_numerals (Abs (_, _, t)) = add_numerals t
   | add_numerals _ = I;
 
-fun mk_number T 0 = Const ("HOL.zero_class.zero", T)
-  | mk_number T 1 = Const ("HOL.one_class.one", T)
+fun mk_number T 0 = Const ("Algebras.zero_class.zero", T)
+  | mk_number T 1 = Const ("Algebras.one_class.one", T)
   | mk_number T i = number_of_const T $ mk_numeral i;
 
-fun dest_number (Const ("HOL.zero_class.zero", T)) = (T, 0)
-  | dest_number (Const ("HOL.one_class.one", T)) = (T, 1)
+fun dest_number (Const ("Algebras.zero_class.zero", T)) = (T, 0)
+  | dest_number (Const ("Algebras.one_class.one", T)) = (T, 1)
   | dest_number (Const ("Int.number_class.number_of", Type ("fun", [_, T])) $ t) =
       (T, dest_numeral t)
   | dest_number t = raise TERM ("dest_number", [t]);
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/inductive.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -184,7 +184,7 @@
     case concl_of thm of
       Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
     | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
-    | _ $ (Const (@{const_name HOL.less_eq}, _) $ _ $ _) =>
+    | _ $ (Const (@{const_name Algebras.less_eq}, _) $ _ $ _) =>
       dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
         (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
     | _ => thm
@@ -561,7 +561,7 @@
          (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds));
 
     val ind_concl = HOLogic.mk_Trueprop
-      (HOLogic.mk_binrel "HOL.ord_class.less_eq" (rec_const, ind_pred));
+      (HOLogic.mk_binrel @{const_name Algebras.less_eq} (rec_const, ind_pred));
 
     val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
 
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/int_arith.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -49,13 +49,13 @@
   make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
   proc = proc1, identifier = []};
 
-fun check (Const (@{const_name HOL.one}, @{typ int})) = false
-  | check (Const (@{const_name HOL.one}, _)) = true
+fun check (Const (@{const_name Algebras.one}, @{typ int})) = false
+  | check (Const (@{const_name Algebras.one}, _)) = true
   | check (Const (s, _)) = member (op =) [@{const_name "op ="},
-      @{const_name HOL.times}, @{const_name HOL.uminus},
-      @{const_name HOL.minus}, @{const_name HOL.plus},
-      @{const_name HOL.zero},
-      @{const_name HOL.less}, @{const_name HOL.less_eq}] s
+      @{const_name Algebras.times}, @{const_name Algebras.uminus},
+      @{const_name Algebras.minus}, @{const_name Algebras.plus},
+      @{const_name Algebras.zero},
+      @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
   | check (a $ b) = check a andalso check b
   | check _ = false;
 
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -138,8 +138,8 @@
 *)
 fun demult (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat =
 let
-  fun demult ((mC as Const (@{const_name HOL.times}, _)) $ s $ t, m) =
-      (case s of Const (@{const_name HOL.times}, _) $ s1 $ s2 =>
+  fun demult ((mC as Const (@{const_name Algebras.times}, _)) $ s $ t, m) =
+      (case s of Const (@{const_name Algebras.times}, _) $ s1 $ s2 =>
         (* bracketing to the right: '(s1 * s2) * t' becomes 's1 * (s2 * t)' *)
         demult (mC $ s1 $ (mC $ s2 $ t), m)
       | _ =>
@@ -150,7 +150,7 @@
               (SOME t', m'') => (SOME (mC $ s' $ t'), m'')
             | (NONE,    m'') => (SOME s', m''))
         | (NONE,    m') => demult (t, m')))
-    | demult ((mC as Const (@{const_name HOL.divide}, _)) $ s $ t, m) =
+    | demult ((mC as Const (@{const_name Algebras.divide}, _)) $ s $ t, m) =
       (* FIXME: Shouldn't we simplify nested quotients, e.g. '(s/t)/u' could
          become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ?   Note that
          if we choose to do so here, the simpset used by arith must be able to
@@ -170,9 +170,9 @@
         (SOME _, _) => (SOME (mC $ s $ t), m)
       | (NONE,  m') => apsnd (Rat.mult (Rat.inv m')) (demult (s, m)))
     (* terms that evaluate to numeric constants *)
-    | demult (Const (@{const_name HOL.uminus}, _) $ t, m) = demult (t, Rat.neg m)
-    | demult (Const (@{const_name HOL.zero}, _), m) = (NONE, Rat.zero)
-    | demult (Const (@{const_name HOL.one}, _), m) = (NONE, m)
+    | demult (Const (@{const_name Algebras.uminus}, _) $ t, m) = demult (t, Rat.neg m)
+    | demult (Const (@{const_name Algebras.zero}, _), m) = (NONE, Rat.zero)
+    | demult (Const (@{const_name Algebras.one}, _), m) = (NONE, m)
     (*Warning: in rare cases number_of encloses a non-numeral,
       in which case dest_numeral raises TERM; hence all the handles below.
       Same for Suc-terms that turn out not to be numerals -
@@ -196,23 +196,23 @@
   (* Turns a term 'all' and associated multiplicity 'm' into a list 'p' of
      summands and associated multiplicities, plus a constant 'i' (with implicit
      multiplicity 1) *)
-  fun poly (Const (@{const_name HOL.plus}, _) $ s $ t,
+  fun poly (Const (@{const_name Algebras.plus}, _) $ s $ t,
         m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = poly (s, m, poly (t, m, pi))
-    | poly (all as Const (@{const_name HOL.minus}, T) $ s $ t, m, pi) =
+    | poly (all as Const (@{const_name Algebras.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 (@{const_name HOL.uminus}, T) $ t, m, pi) =
+    | poly (all as Const (@{const_name Algebras.uminus}, T) $ t, m, pi) =
         if nT T then add_atom all m pi else poly (t, Rat.neg m, pi)
-    | poly (Const (@{const_name HOL.zero}, _), _, pi) =
+    | poly (Const (@{const_name Algebras.zero}, _), _, pi) =
         pi
-    | poly (Const (@{const_name HOL.one}, _), m, (p, i)) =
+    | poly (Const (@{const_name Algebras.one}, _), m, (p, i)) =
         (p, Rat.add i m)
     | poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =
         poly (t, m, (p, Rat.add i m))
-    | poly (all as Const (@{const_name HOL.times}, _) $ _ $ _, m, pi as (p, i)) =
+    | poly (all as Const (@{const_name Algebras.times}, _) $ _ $ _, m, pi as (p, i)) =
         (case demult inj_consts (all, m) of
            (NONE,   m') => (p, Rat.add i m')
          | (SOME u, m') => add_atom u m' pi)
-    | poly (all as Const (@{const_name HOL.divide}, _) $ _ $ _, m, pi as (p, i)) =
+    | poly (all as Const (@{const_name Algebras.divide}, _) $ _ $ _, m, pi as (p, i)) =
         (case demult inj_consts (all, m) of
            (NONE,   m') => (p, Rat.add i m')
          | (SOME u, m') => add_atom u m' pi)
@@ -229,8 +229,8 @@
   val (q, j) = poly (rhs, Rat.one, ([], Rat.zero))
 in
   case rel of
-    @{const_name HOL.less}    => SOME (p, i, "<", q, j)
-  | @{const_name HOL.less_eq} => SOME (p, i, "<=", q, j)
+    @{const_name Algebras.less}    => SOME (p, i, "<", q, j)
+  | @{const_name Algebras.less_eq} => SOME (p, i, "<=", q, j)
   | "op ="              => SOME (p, i, "=", q, j)
   | _                   => NONE
 end handle Rat.DIVZERO => NONE;
@@ -292,11 +292,11 @@
     case head_of lhs of
       Const (a, _) => member (op =) [@{const_name Orderings.max},
                                     @{const_name Orderings.min},
-                                    @{const_name HOL.abs},
-                                    @{const_name HOL.minus},
-                                    "Int.nat",
-                                    "Divides.div_class.mod",
-                                    "Divides.div_class.div"] a
+                                    @{const_name Algebras.abs},
+                                    @{const_name Algebras.minus},
+                                    "Int.nat" (*DYNAMIC BINDING!*),
+                                    "Divides.div_class.mod" (*DYNAMIC BINDING!*),
+                                    "Divides.div_class.div" (*DYNAMIC BINDING!*)] a
     | _            => (warning ("Lin. Arith.: wrong format for split rule " ^
                                  Display.string_of_thm_without_context thm);
                        false))
@@ -372,7 +372,7 @@
         val rev_terms     = rev terms
         val terms1        = map (subst_term [(split_term, t1)]) rev_terms
         val terms2        = map (subst_term [(split_term, t2)]) rev_terms
-        val t1_leq_t2     = Const (@{const_name HOL.less_eq},
+        val t1_leq_t2     = Const (@{const_name Algebras.less_eq},
                                     split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
         val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
         val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -387,7 +387,7 @@
         val rev_terms     = rev terms
         val terms1        = map (subst_term [(split_term, t1)]) rev_terms
         val terms2        = map (subst_term [(split_term, t2)]) rev_terms
-        val t1_leq_t2     = Const (@{const_name HOL.less_eq},
+        val t1_leq_t2     = Const (@{const_name Algebras.less_eq},
                                     split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
         val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
         val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -397,16 +397,16 @@
         SOME [(Ts, subgoal1), (Ts, subgoal2)]
       end
     (* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
-    | (Const (@{const_name HOL.abs}, _), [t1]) =>
+    | (Const (@{const_name Algebras.abs}, _), [t1]) =>
       let
         val rev_terms   = rev terms
         val terms1      = map (subst_term [(split_term, t1)]) rev_terms
-        val terms2      = map (subst_term [(split_term, Const (@{const_name HOL.uminus},
+        val terms2      = map (subst_term [(split_term, Const (@{const_name Algebras.uminus},
                             split_type --> split_type) $ t1)]) rev_terms
-        val zero        = Const (@{const_name HOL.zero}, split_type)
-        val zero_leq_t1 = Const (@{const_name HOL.less_eq},
+        val zero        = Const (@{const_name Algebras.zero}, split_type)
+        val zero_leq_t1 = Const (@{const_name Algebras.less_eq},
                             split_type --> split_type --> HOLogic.boolT) $ zero $ t1
-        val t1_lt_zero  = Const (@{const_name HOL.less},
+        val t1_lt_zero  = Const (@{const_name Algebras.less},
                             split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
         val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1    = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
@@ -415,22 +415,22 @@
         SOME [(Ts, subgoal1), (Ts, subgoal2)]
       end
     (* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *)
-    | (Const (@{const_name HOL.minus}, _), [t1, t2]) =>
+    | (Const (@{const_name Algebras.minus}, _), [t1, t2]) =>
       let
         (* "d" in the above theorem becomes a new bound variable after NNF   *)
         (* transformation, therefore some adjustment of indices is necessary *)
         val rev_terms       = rev terms
-        val zero            = Const (@{const_name HOL.zero}, split_type)
+        val zero            = Const (@{const_name Algebras.zero}, split_type)
         val d               = Bound 0
         val terms1          = map (subst_term [(split_term, zero)]) rev_terms
         val terms2          = map (subst_term [(incr_boundvars 1 split_term, d)])
                                 (map (incr_boundvars 1) rev_terms)
         val t1'             = incr_boundvars 1 t1
         val t2'             = incr_boundvars 1 t2
-        val t1_lt_t2        = Const (@{const_name HOL.less},
+        val t1_lt_t2        = Const (@{const_name Algebras.less},
                                 split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
         val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
-                                (Const (@{const_name HOL.plus},
+                                (Const (@{const_name Algebras.plus},
                                   split_type --> split_type --> split_type) $ t2' $ d)
         val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1        = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
@@ -442,8 +442,8 @@
     | (Const ("Int.nat", _), [t1]) =>
       let
         val rev_terms   = rev terms
-        val zero_int    = Const (@{const_name HOL.zero}, HOLogic.intT)
-        val zero_nat    = Const (@{const_name HOL.zero}, HOLogic.natT)
+        val zero_int    = Const (@{const_name Algebras.zero}, HOLogic.intT)
+        val zero_nat    = Const (@{const_name Algebras.zero}, HOLogic.natT)
         val n           = Bound 0
         val terms1      = map (subst_term [(incr_boundvars 1 split_term, n)])
                             (map (incr_boundvars 1) rev_terms)
@@ -451,7 +451,7 @@
         val t1'         = incr_boundvars 1 t1
         val t1_eq_nat_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
                             (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
-        val t1_lt_zero  = Const (@{const_name HOL.less},
+        val t1_lt_zero  = Const (@{const_name Algebras.less},
                             HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
         val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1    = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false]
@@ -465,7 +465,7 @@
     | (Const ("Divides.div_class.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
-        val zero                    = Const (@{const_name HOL.zero}, split_type)
+        val zero                    = Const (@{const_name Algebras.zero}, split_type)
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
@@ -477,11 +477,11 @@
                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
         val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
-        val j_lt_t2                 = Const (@{const_name HOL.less},
+        val j_lt_t2                 = Const (@{const_name Algebras.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
-                                       (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
-                                         (Const (@{const_name HOL.times},
+                                       (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
+                                         (Const (@{const_name Algebras.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
@@ -497,7 +497,7 @@
     | (Const ("Divides.div_class.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
-        val zero                    = Const (@{const_name HOL.zero}, split_type)
+        val zero                    = Const (@{const_name Algebras.zero}, split_type)
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
@@ -509,11 +509,11 @@
                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
         val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
-        val j_lt_t2                 = Const (@{const_name HOL.less},
+        val j_lt_t2                 = Const (@{const_name Algebras.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
-                                       (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
-                                         (Const (@{const_name HOL.times},
+                                       (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
+                                         (Const (@{const_name Algebras.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
@@ -535,7 +535,7 @@
         Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
-        val zero                    = Const (@{const_name HOL.zero}, split_type)
+        val zero                    = Const (@{const_name Algebras.zero}, split_type)
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
@@ -545,21 +545,21 @@
         val t2'                     = incr_boundvars 2 t2
         val t2_eq_zero              = Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
-        val zero_lt_t2              = Const (@{const_name HOL.less},
+        val zero_lt_t2              = Const (@{const_name Algebras.less},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
-        val t2_lt_zero              = Const (@{const_name HOL.less},
+        val t2_lt_zero              = Const (@{const_name Algebras.less},
                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
-        val zero_leq_j              = Const (@{const_name HOL.less_eq},
+        val zero_leq_j              = Const (@{const_name Algebras.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
-        val j_leq_zero              = Const (@{const_name HOL.less_eq},
+        val j_leq_zero              = Const (@{const_name Algebras.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ j $ zero
-        val j_lt_t2                 = Const (@{const_name HOL.less},
+        val j_lt_t2                 = Const (@{const_name Algebras.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
-        val t2_lt_j                 = Const (@{const_name HOL.less},
+        val t2_lt_j                 = Const (@{const_name Algebras.less},
                                         split_type --> split_type--> HOLogic.boolT) $ t2' $ j
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
-                                       (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
-                                         (Const (@{const_name HOL.times},
+                                       (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
+                                         (Const (@{const_name Algebras.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
@@ -589,7 +589,7 @@
         Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
-        val zero                    = Const (@{const_name HOL.zero}, split_type)
+        val zero                    = Const (@{const_name Algebras.zero}, split_type)
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
@@ -599,21 +599,21 @@
         val t2'                     = incr_boundvars 2 t2
         val t2_eq_zero              = Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
-        val zero_lt_t2              = Const (@{const_name HOL.less},
+        val zero_lt_t2              = Const (@{const_name Algebras.less},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
-        val t2_lt_zero              = Const (@{const_name HOL.less},
+        val t2_lt_zero              = Const (@{const_name Algebras.less},
                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
-        val zero_leq_j              = Const (@{const_name HOL.less_eq},
+        val zero_leq_j              = Const (@{const_name Algebras.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
-        val j_leq_zero              = Const (@{const_name HOL.less_eq},
+        val j_leq_zero              = Const (@{const_name Algebras.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ j $ zero
-        val j_lt_t2                 = Const (@{const_name HOL.less},
+        val j_lt_t2                 = Const (@{const_name Algebras.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
-        val t2_lt_j                 = Const (@{const_name HOL.less},
+        val t2_lt_j                 = Const (@{const_name Algebras.less},
                                         split_type --> split_type--> HOLogic.boolT) $ t2' $ j
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
-                                       (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
-                                         (Const (@{const_name HOL.times},
+                                       (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
+                                         (Const (@{const_name Algebras.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/meson.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -403,7 +403,7 @@
       (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
 
 (*A higher-order instance of a first-order constant? Example is the definition of
-  HOL.one, 1, at a function type in theory SetsAndFunctions.*)
+  one, 1, at a function type in theory SetsAndFunctions.*)
 fun higher_inst_const thy (c,T) =
   case binder_types T of
       [] => false (*not a function type, OK*)
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/nat_arith.ML
--- a/src/HOL/Tools/nat_arith.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/nat_arith.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -19,8 +19,8 @@
 
 (** abstract syntax of structure nat: 0, Suc, + **)
 
-val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
-val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
+val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus};
+val dest_plus = HOLogic.dest_bin @{const_name Algebras.plus} HOLogic.natT;
 
 fun mk_sum [] = HOLogic.zero
   | mk_sum [t] = t
@@ -69,24 +69,24 @@
 structure LessCancelSums = CancelSumsFun
 (struct
   open CommonCancelSums;
-  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
+  val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less};
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT;
   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
 end);
 
 structure LeCancelSums = CancelSumsFun
 (struct
   open CommonCancelSums;
-  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
+  val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq};
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT;
   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
 end);
 
 structure DiffCancelSums = CancelSumsFun
 (struct
   open CommonCancelSums;
-  val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
+  val mk_bal = HOLogic.mk_binop @{const_name Algebras.minus};
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.minus} HOLogic.natT;
   val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
 end);
 
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -32,7 +32,7 @@
   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
 
 val zero = mk_number 0;
-val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
+val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus};
 
 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
 fun mk_sum []        = zero
@@ -43,7 +43,7 @@
 fun long_mk_sum []        = HOLogic.zero
   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
 
-val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
+val dest_plus = HOLogic.dest_bin @{const_name Algebras.plus} HOLogic.natT;
 
 
 (** Other simproc items **)
@@ -61,14 +61,14 @@
 (*** CancelNumerals simprocs ***)
 
 val one = mk_number 1;
-val mk_times = HOLogic.mk_binop @{const_name HOL.times};
+val mk_times = HOLogic.mk_binop @{const_name Algebras.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 @{const_name HOL.times} HOLogic.natT;
+val dest_times = HOLogic.dest_bin @{const_name Algebras.times} HOLogic.natT;
 
 fun dest_prod t =
       let val (t,u) = dest_times t
@@ -176,8 +176,8 @@
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
   val bal_add1 = @{thm nat_less_add_iff1} RS trans
   val bal_add2 = @{thm nat_less_add_iff2} RS trans
 );
@@ -185,8 +185,8 @@
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
   val bal_add1 = @{thm nat_le_add_iff1} RS trans
   val bal_add2 = @{thm nat_le_add_iff2} RS trans
 );
@@ -194,8 +194,8 @@
 structure DiffCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binop @{const_name HOL.minus}
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binop @{const_name Algebras.minus}
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.minus} HOLogic.natT
   val bal_add1 = @{thm nat_diff_add_eq1} RS trans
   val bal_add2 = @{thm nat_diff_add_eq2} RS trans
 );
@@ -308,8 +308,8 @@
 structure LessCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
   val cancel = @{thm nat_mult_less_cancel1} RS trans
   val neg_exchanges = true
 )
@@ -317,8 +317,8 @@
 structure LeCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
   val cancel = @{thm nat_mult_le_cancel1} RS trans
   val neg_exchanges = true
 )
@@ -387,16 +387,16 @@
 structure LessCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
   fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj}
 );
 
 structure LeCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
   fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj}
 );
 
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -34,12 +34,12 @@
 val long_mk_sum = Arith_Data.long_mk_sum;
 val dest_sum = Arith_Data.dest_sum;
 
-val mk_diff = HOLogic.mk_binop @{const_name HOL.minus};
-val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT;
+val mk_diff = HOLogic.mk_binop @{const_name Algebras.minus};
+val dest_diff = HOLogic.dest_bin @{const_name Algebras.minus} Term.dummyT;
 
-val mk_times = HOLogic.mk_binop @{const_name HOL.times};
+val mk_times = HOLogic.mk_binop @{const_name Algebras.times};
 
-fun one_of T = Const(@{const_name HOL.one},T);
+fun one_of T = Const(@{const_name Algebras.one}, T);
 
 (* build product with trailing 1 rather than Numeral 1 in order to avoid the
    unnecessary restriction to type class number_ring
@@ -56,7 +56,7 @@
 fun long_mk_prod T []        = one_of T
   | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
 
-val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT;
+val dest_times = HOLogic.dest_bin @{const_name Algebras.times} Term.dummyT;
 
 fun dest_prod t =
       let val (t,u) = dest_times t
@@ -72,7 +72,7 @@
 fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
 
 (*Express t as a product of (possibly) a numeral with other sorted terms*)
-fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t
+fun dest_coeff sign (Const (@{const_name Algebras.uminus}, _) $ t) = dest_coeff (~sign) t
   | dest_coeff sign t =
     let val ts = sort TermOrd.term_ord (dest_prod t)
         val (n, ts') = find_first_numeral [] ts
@@ -96,7 +96,7 @@
   Fractions are reduced later by the cancel_numeral_factor simproc.*)
 fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
 
-val mk_divide = HOLogic.mk_binop @{const_name HOL.divide};
+val mk_divide = HOLogic.mk_binop @{const_name Algebras.divide};
 
 (*Build term (p / q) * t*)
 fun mk_fcoeff ((p, q), t) =
@@ -104,8 +104,8 @@
   in mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
 
 (*Express t as a product of a fraction with other sorted terms*)
-fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t
-  | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) =
+fun dest_fcoeff sign (Const (@{const_name Algebras.uminus}, _) $ t) = dest_fcoeff (~sign) t
+  | dest_fcoeff sign (Const (@{const_name Algebras.divide}, _) $ t $ u) =
     let val (p, t') = dest_coeff sign t
         val (q, u') = dest_coeff 1 u
     in (mk_frac (p, q), mk_divide (t', u')) end
@@ -230,8 +230,8 @@
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
   val bal_add1 = @{thm less_add_iff1} RS trans
   val bal_add2 = @{thm less_add_iff2} RS trans
 );
@@ -239,8 +239,8 @@
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
   val bal_add1 = @{thm le_add_iff1} RS trans
   val bal_add2 = @{thm le_add_iff2} RS trans
 );
@@ -392,8 +392,8 @@
 structure DivideCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
+  val mk_bal   = HOLogic.mk_binop @{const_name Algebras.divide}
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
   val cancel = @{thm mult_divide_mult_cancel_left} RS trans
   val neg_exchanges = false
 )
@@ -410,8 +410,8 @@
 structure LessCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
   val cancel = @{thm mult_less_cancel_left} RS trans
   val neg_exchanges = true
 )
@@ -419,8 +419,8 @@
 structure LeCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
   val cancel = @{thm mult_le_cancel_left} RS trans
   val neg_exchanges = true
 )
@@ -485,8 +485,8 @@
 in
 fun sign_conv pos_th neg_th ss t =
   let val T = fastype_of t;
-      val zero = Const(@{const_name HOL.zero}, T);
-      val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
+      val zero = Const(@{const_name Algebras.zero}, T);
+      val less = Const(@{const_name Algebras.less}, [T,T] ---> HOLogic.boolT);
       val pos = less $ zero $ t and neg = less $ t $ zero
       fun prove p =
         Option.map Eq_True_elim (Lin_Arith.simproc ss p)
@@ -525,8 +525,8 @@
 structure LeCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
   val simp_conv = sign_conv
     @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
 );
@@ -535,8 +535,8 @@
 structure LessCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
   val simp_conv = sign_conv
     @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
 );
@@ -571,8 +571,8 @@
 structure DivideCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
+  val mk_bal   = HOLogic.mk_binop @{const_name Algebras.divide}
+  val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
   fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
 );
 
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/refute.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -708,13 +708,13 @@
       (* other optimizations *)
       | Const (@{const_name Finite_Set.card}, _) => t
       | Const (@{const_name Finite_Set.finite}, _) => t
-      | Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
+      | Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
-      | Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
+      | Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
-      | Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []),
+      | Const (@{const_name Algebras.minus}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
-      | Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
+      | Const (@{const_name Algebras.times}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
       | Const (@{const_name List.append}, _) => t
       | Const (@{const_name lfp}, _) => t
@@ -883,16 +883,16 @@
       | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
       | Const (@{const_name Finite_Set.finite}, T) =>
         collect_type_axioms T axs
-      | Const (@{const_name HOL.less}, T as Type ("fun", [Type ("nat", []),
+      | Const (@{const_name Algebras.less}, T as Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
           collect_type_axioms T axs
-      | Const (@{const_name HOL.plus}, T as Type ("fun", [Type ("nat", []),
+      | Const (@{const_name Algebras.plus}, T as Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
           collect_type_axioms T axs
-      | Const (@{const_name HOL.minus}, T as Type ("fun", [Type ("nat", []),
+      | Const (@{const_name Algebras.minus}, T as Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
           collect_type_axioms T axs
-      | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []),
+      | Const (@{const_name Algebras.times}, T as Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
           collect_type_axioms T axs
       | Const (@{const_name List.append}, T) => collect_type_axioms T axs
@@ -2765,13 +2765,13 @@
   (* theory -> model -> arguments -> Term.term ->
     (interpretation * model * arguments) option *)
 
-  (* only an optimization: 'HOL.less' could in principle be interpreted with *)
+  (* only an optimization: 'less' could in principle be interpreted with *)
   (* interpreters available already (using its definition), but the code     *)
   (* below is more efficient                                                 *)
 
   fun Nat_less_interpreter thy model args t =
     case t of
-      Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
+      Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
       let
         val size_of_nat = size_of_type thy model (Type ("nat", []))
@@ -2788,13 +2788,13 @@
   (* theory -> model -> arguments -> Term.term ->
     (interpretation * model * arguments) option *)
 
-  (* only an optimization: 'HOL.plus' could in principle be interpreted with *)
+  (* only an optimization: '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 (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
+      Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
       let
         val size_of_nat = size_of_type thy model (Type ("nat", []))
@@ -2819,13 +2819,13 @@
   (* theory -> model -> arguments -> Term.term ->
     (interpretation * model * arguments) option *)
 
-  (* only an optimization: 'HOL.minus' could in principle be interpreted *)
+  (* only an optimization: 'minus' could in principle be interpreted *)
   (* with interpreters available already (using its definition), but the *)
   (* code below is more efficient                                        *)
 
   fun Nat_minus_interpreter thy model args t =
     case t of
-      Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []),
+      Const (@{const_name Algebras.minus}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
       let
         val size_of_nat = size_of_type thy model (Type ("nat", []))
@@ -2847,13 +2847,13 @@
   (* theory -> model -> arguments -> Term.term ->
     (interpretation * model * arguments) option *)
 
-  (* only an optimization: 'HOL.times' could in principle be interpreted *)
+  (* only an optimization: 'times' could in principle be interpreted *)
   (* with interpreters available already (using its definition), but the *)
   (* code below is more efficient                                        *)
 
   fun Nat_times_interpreter thy model args t =
     case t of
-      Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
+      Const (@{const_name Algebras.times}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
       let
         val size_of_nat = size_of_type thy model (Type ("nat", []))
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/res_clause.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -99,7 +99,7 @@
 (*Provide readable names for the more common symbolic functions*)
 val const_trans_table =
       Symtab.make [(@{const_name "op ="}, "equal"),
-                   (@{const_name HOL.less_eq}, "lessequals"),
+                   (@{const_name Algebras.less_eq}, "lessequals"),
                    (@{const_name "op &"}, "and"),
                    (@{const_name "op |"}, "or"),
                    (@{const_name "op -->"}, "implies"),
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Transcendental.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -36,7 +36,7 @@
 apply (subst setsum_op_ivl_Suc)
 apply (subst lemma_realpow_diff_sumr)
 apply (simp add: right_distrib del: setsum_op_ivl_Suc)
-apply (subst mult_left_commute [where a="x - y"])
+apply (subst mult_left_commute [of "x - y"])
 apply (erule subst)
 apply (simp add: algebra_simps)
 done
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/ex/Arith_Examples.thy
--- a/src/HOL/ex/Arith_Examples.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/ex/Arith_Examples.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -33,7 +33,7 @@
 *)
 
 subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
-           @{term HOL.minus}, @{term nat}, @{term Divides.mod},
+           @{term Algebras.minus}, @{term nat}, @{term Divides.mod},
            @{term Divides.div} *}
 
 lemma "(i::nat) <= max i j"
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/ex/Binary.thy
--- a/src/HOL/ex/Binary.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/ex/Binary.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -27,8 +27,8 @@
     | dest_bit (Const (@{const_name True}, _)) = 1
     | dest_bit t = raise TERM ("dest_bit", [t]);
 
-  fun dest_binary (Const (@{const_name HOL.zero}, Type (@{type_name nat}, _))) = 0
-    | dest_binary (Const (@{const_name HOL.one}, Type (@{type_name nat}, _))) = 1
+  fun dest_binary (Const (@{const_name Algebras.zero}, Type (@{type_name nat}, _))) = 0
+    | dest_binary (Const (@{const_name Algebras.one}, Type (@{type_name nat}, _))) = 1
     | dest_binary (Const (@{const_name bit}, _) $ bs $ b) = 2 * dest_binary bs + dest_bit b
     | dest_binary t = raise TERM ("dest_binary", [t]);
 
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/ex/SVC_Oracle.thy
--- a/src/HOL/ex/SVC_Oracle.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -63,21 +63,21 @@
     (*abstraction of a numeric literal*)
     fun lit t = if can HOLogic.dest_number t then t else replace t;
     (*abstraction of a real/rational expression*)
-    fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
-      | rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
-      | rat ((c as Const(@{const_name HOL.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
-      | rat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
-      | rat ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (rat x)
+    fun rat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+      | rat ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+      | rat ((c as Const(@{const_name Algebras.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+      | rat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+      | rat ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (rat x)
       | rat t = lit t
     (*abstraction of an integer expression: no div, mod*)
-    fun int ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
-      | int ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
-      | int ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (int x) $ (int y)
-      | int ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (int x)
+    fun int ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
+      | int ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
+      | int ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (int x) $ (int y)
+      | int ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (int x)
       | int t = lit t
     (*abstraction of a natural number expression: no minus*)
-    fun nat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
-      | nat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
+    fun nat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
+      | nat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
       | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
       | nat t = lit t
     (*abstraction of a relation: =, <, <=*)
@@ -95,8 +95,8 @@
       | fm ((c as Const("True", _))) = c
       | fm ((c as Const("False", _))) = c
       | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
-      | fm (t as Const(@{const_name HOL.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
-      | fm (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+      | fm (t as Const(@{const_name Algebras.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+      | fm (t as Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
       | fm t = replace t
     (*entry point, and abstraction of a meta-formula*)
     fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
diff -r ae634fad947e -r 18b41bba42b5 src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/ex/svc_funcs.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -107,8 +107,8 @@
                          b1 orelse b2)
                      end
                  else (*might be numeric equality*) (t, is_intnat T)
-           | Const(@{const_name HOL.less}, Type ("fun", [T,_]))  => (t, is_intnat T)
-           | Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
+           | Const(@{const_name Algebras.less}, Type ("fun", [T,_]))  => (t, is_intnat T)
+           | Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
            | _ => (t, false)
          end
    in #1 o tag end;
@@ -146,16 +146,16 @@
     (*translation of a literal*)
     val lit = snd o HOLogic.dest_number;
     (*translation of a literal expression [no variables]*)
-    fun litExp (Const(@{const_name HOL.plus}, T) $ x $ y) =
+    fun litExp (Const(@{const_name Algebras.plus}, T) $ x $ y) =
           if is_numeric_op T then (litExp x) + (litExp y)
           else fail t
-      | litExp (Const(@{const_name HOL.minus}, T) $ x $ y) =
+      | litExp (Const(@{const_name Algebras.minus}, T) $ x $ y) =
           if is_numeric_op T then (litExp x) - (litExp y)
           else fail t
-      | litExp (Const(@{const_name HOL.times}, T) $ x $ y) =
+      | litExp (Const(@{const_name Algebras.times}, T) $ x $ y) =
           if is_numeric_op T then (litExp x) * (litExp y)
           else fail t
-      | litExp (Const(@{const_name HOL.uminus}, T) $ x)   =
+      | litExp (Const(@{const_name Algebras.uminus}, T) $ x)   =
           if is_numeric_op T then ~(litExp x)
           else fail t
       | litExp t = lit t
@@ -163,21 +163,21 @@
     (*translation of a real/rational expression*)
     fun suc t = Interp("+", [Int 1, t])
     fun tm (Const(@{const_name Suc}, T) $ x) = suc (tm x)
-      | tm (Const(@{const_name HOL.plus}, T) $ x $ y) =
+      | tm (Const(@{const_name Algebras.plus}, T) $ x $ y) =
           if is_numeric_op T then Interp("+", [tm x, tm y])
           else fail t
-      | tm (Const(@{const_name HOL.minus}, T) $ x $ y) =
+      | tm (Const(@{const_name Algebras.minus}, T) $ x $ y) =
           if is_numeric_op T then
               Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
           else fail t
-      | tm (Const(@{const_name HOL.times}, T) $ x $ y) =
+      | tm (Const(@{const_name Algebras.times}, T) $ x $ y) =
           if is_numeric_op T then Interp("*", [tm x, tm y])
           else fail t
-      | tm (Const(@{const_name HOL.inverse}, T) $ x) =
+      | tm (Const(@{const_name Algebras.inverse}, T) $ x) =
           if domain_type T = HOLogic.realT then
               Rat(1, litExp x)
           else fail t
-      | tm (Const(@{const_name HOL.uminus}, T) $ x) =
+      | tm (Const(@{const_name Algebras.uminus}, T) $ x) =
           if is_numeric_op T then Interp("*", [Int ~1, tm x])
           else fail t
       | tm t = Int (lit t)
@@ -211,13 +211,13 @@
                    else fail t
             end
         (*inequalities: possible types are nat, int, real*)
-      | fm pos (t as Const(@{const_name HOL.less},  Type ("fun", [T,_])) $ x $ y) =
+      | fm pos (t as Const(@{const_name Algebras.less},  Type ("fun", [T,_])) $ x $ y) =
             if not pos orelse T = HOLogic.realT then
                 Buildin("<", [tm x, tm y])
             else if is_intnat T then
                 Buildin("<=", [suc (tm x), tm y])
             else fail t
-      | fm pos (t as Const(@{const_name HOL.less_eq},  Type ("fun", [T,_])) $ x $ y) =
+      | fm pos (t as Const(@{const_name Algebras.less_eq},  Type ("fun", [T,_])) $ x $ y) =
             if pos orelse T = HOLogic.realT then
                 Buildin("<=", [tm x, tm y])
             else if is_intnat T then
diff -r ae634fad947e -r 18b41bba42b5 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -719,7 +719,7 @@
   val take_stricts' = rewrite_rule copy_take_defs take_stricts;
   fun take_0 n dn =
     let
-      val goal = mk_trp ((dc_take dn $ %%:"HOL.zero") `% x_name n === UU);
+      val goal = mk_trp ((dc_take dn $ %%: @{const_name Algebras.zero}) `% x_name n === UU);
     in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
   val take_0s = mapn take_0 1 dnames;
   fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts'::copy_con_rews) 1;
diff -r ae634fad947e -r 18b41bba42b5 src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/Provers/Arith/abel_cancel.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -28,29 +28,29 @@
 
 (* FIXME dependent on abstract syntax *)
 
-fun zero t = Const (@{const_name HOL.zero}, t);
-fun minus t = Const (@{const_name HOL.uminus}, t --> t);
+fun zero t = Const (@{const_name Algebras.zero}, t);
+fun minus t = Const (@{const_name Algebras.uminus}, t --> t);
 
-fun add_terms pos (Const (@{const_name HOL.plus}, _) $ x $ y, ts) =
+fun add_terms pos (Const (@{const_name Algebras.plus}, _) $ x $ y, ts) =
       add_terms pos (x, add_terms pos (y, ts))
-  | add_terms pos (Const (@{const_name HOL.minus}, _) $ x $ y, ts) =
+  | add_terms pos (Const (@{const_name Algebras.minus}, _) $ x $ y, ts) =
       add_terms pos (x, add_terms (not pos) (y, ts))
-  | add_terms pos (Const (@{const_name HOL.uminus}, _) $ x, ts) =
+  | add_terms pos (Const (@{const_name Algebras.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(@{const_name HOL.plus},_)) $ x $ y) =
+fun zero1 pt (u as (c as Const(@{const_name Algebras.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(@{const_name HOL.minus},_)) $ x $ y) =
+  | zero1 (pos,t) (u as (c as Const(@{const_name Algebras.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(@{const_name HOL.uminus},_)) $ x) =
+  | zero1 (pos,t) (u as (c as Const(@{const_name Algebras.uminus},_)) $ x) =
       (case zero1 (not pos,t) x of NONE => NONE
        | SOME z => SOME(c $ z))
   | zero1 (pos,t) u =
@@ -71,7 +71,7 @@
 fun cancel t =
   let
     val c $ lhs $ rhs = t
-    val opp = case c of Const(@{const_name HOL.plus},_) => true | _ => false;
+    val opp = case c of Const(@{const_name Algebras.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 ae634fad947e -r 18b41bba42b5 src/Provers/Arith/cancel_div_mod.ML
--- a/src/Provers/Arith/cancel_div_mod.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/Provers/Arith/cancel_div_mod.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Provers/Arith/cancel_div_mod.ML
-    ID:         $Id$
     Author:     Tobias Nipkow, TU Muenchen
 
 Cancel div and mod terms:
@@ -7,7 +6,7 @@
   A + n*(m div n) + B + (m mod n) + C  ==  A + B + C + m
 
 FIXME: Is parameterized but assumes for simplicity that + and * are named
-HOL.plus and HOL.minus
+as in HOL
 *)
 
 signature CANCEL_DIV_MOD_DATA =
@@ -35,12 +34,12 @@
 functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
 struct
 
-fun coll_div_mod (Const(@{const_name HOL.plus},_) $ s $ t) dms =
+fun coll_div_mod (Const(@{const_name Algebras.plus},_) $ s $ t) dms =
       coll_div_mod t (coll_div_mod s dms)
-  | coll_div_mod (Const(@{const_name HOL.times},_) $ m $ (Const(d,_) $ s $ n))
+  | coll_div_mod (Const(@{const_name Algebras.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(@{const_name HOL.times},_) $ (Const(d,_) $ s $ n) $ m)
+  | coll_div_mod (Const(@{const_name Algebras.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 +55,8 @@
    ==> thesis by transitivity
 *)
 
-val mk_plus = Data.mk_binop @{const_name HOL.plus};
-val mk_times = Data.mk_binop @{const_name HOL.times};
+val mk_plus = Data.mk_binop @{const_name Algebras.plus};
+val mk_times = Data.mk_binop @{const_name Algebras.times};
 
 fun rearrange t pq =
   let val ts = Data.dest_sum t;