--- a/src/HOL/ex/Refute_Examples.thy Thu Nov 18 14:02:29 2004 +0100
+++ b/src/HOL/ex/Refute_Examples.thy Thu Nov 18 18:46:09 2004 +0100
@@ -8,7 +8,9 @@
header {* Examples for the 'refute' command *}
-theory Refute_Examples = Main:
+theory Refute_Examples imports Main
+
+begin
lemma "P x"
refute