--- a/src/HOL/Library/comm_ring.ML Fri Oct 12 08:25:47 2007 +0200
+++ b/src/HOL/Library/comm_ring.ML Fri Oct 12 08:25:48 2007 +0200
@@ -61,7 +61,7 @@
polex_mul T $ reif_polex T vs a $ reif_polex T vs b
| reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) =
polex_neg T $ reif_polex T vs a
- | reif_polex T vs (Const (@{const_name Nat.power}, _) $ a $ n) =
+ | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
polex_pow T $ reif_polex T vs a $ n
| reif_polex T vs t = polex_pol T $ reif_pol T vs t;