--- 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;
--- a/src/HOL/HOL_lemmas.ML Fri Nov 10 19:02:37 2000 +0100
+++ b/src/HOL/HOL_lemmas.ML Fri Nov 10 19:03:06 2000 +0100
@@ -11,7 +11,6 @@
val plusI = thm "plusI";
val minusI = thm "minusI";
val timesI = thm "timesI";
-val powerI = thm "powerI";
val eq_reflection = thm "eq_reflection";
val refl = thm "refl";
val subst = thm "subst";