--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Fri Feb 19 14:47:00 2010 +0100
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Fri Feb 19 14:47:01 2010 +0100
@@ -13,8 +13,8 @@
struct
(* Zero and One of the commutative ring *)
-fun cring_zero T = Const (@{const_name Algebras.zero}, T);
-fun cring_one T = Const (@{const_name Algebras.one}, T);
+fun cring_zero T = Const (@{const_name Groups.zero}, T);
+fun cring_one T = Const (@{const_name Groups.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 Algebras.plus}, _) $ a $ b) =
+fun reif_polex T vs (Const (@{const_name Groups.plus}, _) $ a $ b) =
polex_add T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name Algebras.minus}, _) $ a $ b) =
+ | reif_polex T vs (Const (@{const_name Groups.minus}, _) $ a $ b) =
polex_sub T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name Algebras.times}, _) $ a $ b) =
+ | reif_polex T vs (Const (@{const_name Groups.times}, _) $ a $ b) =
polex_mul T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name Algebras.uminus}, _) $ a) =
+ | reif_polex T vs (Const (@{const_name Groups.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