avoid using "prop_logic.ML" and "sat_solver.ML" twice (the other occurrence being in "FunDef.thy");
this produces two copies of the same module, with separate references etc.
--- a/src/HOL/Refute.thy Mon Dec 07 11:44:49 2009 +0100
+++ b/src/HOL/Refute.thy Mon Dec 07 11:46:13 2009 +0100
@@ -10,8 +10,6 @@
theory Refute
imports Hilbert_Choice List
uses
- "Tools/prop_logic.ML"
- "Tools/sat_solver.ML"
"Tools/refute.ML"
"Tools/refute_isar.ML"
begin