# HG changeset patch
# User nipkow
# Date 880730250 -3600
# Node ID 44364221a99db5e2a475448c2bef3cad846f3299
# Parent  2335f6584a1b562df8dbbfe3c0b59027e8b794e4
Removed "open Mutil;"

diff -r 2335f6584a1b -r 44364221a99d src/HOL/Induct/Mutil.ML
--- 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 **)