src/HOL/Induct/Sexp.ML
changeset 11481 c77e5401f2ff
parent 8840 18b76c137c41
--- a/src/HOL/Induct/Sexp.ML	Wed Aug 08 14:50:28 2001 +0200
+++ b/src/HOL/Induct/Sexp.ML	Wed Aug 08 14:51:10 2001 +0200
@@ -6,8 +6,6 @@
 S-expressions, general binary trees for defining recursive data structures
 *)
 
-open Sexp;
-
 (** sexp_case **)
 
 Goalw [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";