# HG changeset patch
# User blanchet
# Date 1260182773 -3600
# Node ID 39f21f7bad7e26c8f48e1365f1d18f142002e04c
# Parent  ef2776c8979986438046a57587a126564c79b266
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.

diff -r ef2776c89799 -r 39f21f7bad7e src/HOL/Refute.thy
--- 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