src/HOL/Refute.thy

--- a/src/HOL/Refute.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Refute.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -8,12 +8,13 @@
 
 header {* Refute *}
 
-theory Refute = Map
-
+theory Refute
+import Map
 files "Tools/prop_logic.ML"
       "Tools/sat_solver.ML"
       "Tools/refute.ML"
-      "Tools/refute_isar.ML":
+      "Tools/refute_isar.ML"
+begin
 
 setup Refute.setup