src/HOL/HOL.ML

--- a/src/HOL/HOL.ML	Tue Sep 06 16:29:39 2005 +0200
+++ b/src/HOL/HOL.ML	Tue Sep 06 16:59:48 2005 +0200
@@ -5,9 +5,6 @@
 structure HOL =
 struct
   val thy = the_context ();
-  val plusI = plusI;
-  val minusI = minusI;
-  val timesI = timesI;
   val eq_reflection = eq_reflection;
   val refl = refl;
   val subst = subst;