--- a/src/HOL/Induct/Mutil.ML Fri Nov 28 11:00:42 1997 +0100
+++ b/src/HOL/Induct/Mutil.ML Fri Nov 28 16:17:30 1997 +0100
@@ -6,8 +6,6 @@
The Mutilated Chess Board Problem, formalized inductively
*)
-open Mutil;
-
Addsimps tiling.intrs;
(** The union of two disjoint tilings is a tiling **)