--- a/src/HOL/Induct/Exp.ML Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Induct/Exp.ML Fri Jul 31 10:48:42 1998 +0200
@@ -6,8 +6,6 @@
Example of Mutual Induction via Iteratived Inductive Definitions: Expressions
*)
-open Exp;
-
AddSIs [eval.N, eval.X];
AddIs [eval.Op, eval.valOf];