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}
 );