diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Induct/Exp.ML
--- 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];