--- a/src/HOL/HOL.ML Fri Nov 10 19:02:37 2000 +0100
+++ b/src/HOL/HOL.ML Fri Nov 10 19:03:06 2000 +0100
@@ -8,7 +8,6 @@
val plusI = plusI;
val minusI = minusI;
val timesI = timesI;
- val powerI = powerI;
val eq_reflection = eq_reflection;
val refl = refl;
val subst = subst;