diff -r 939ca97f5a11 -r 1fe9fc908ec3 src/Tools/auto_solve.ML
--- a/src/Tools/auto_solve.ML	Thu Oct 29 11:26:47 2009 +0100
+++ b/src/Tools/auto_solve.ML	Thu Oct 29 11:56:02 2009 +0100
@@ -5,7 +5,7 @@
 existing theorem.  Duplicate lemmas can be detected in this way.
 
 The implementation is based in part on Berghofer and Haftmann's
-quickcheck.ML.  It relies critically on the FindTheorems solves
+quickcheck.ML.  It relies critically on the Find_Theorems solves
 feature.
 *)
 
@@ -45,8 +45,8 @@
   let
     val ctxt = Proof.context_of state;
 
-    val crits = [(true, FindTheorems.Solves)];
-    fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
+    val crits = [(true, Find_Theorems.Solves)];
+    fun find g = snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
 
     fun prt_result (goal, results) =
       let
@@ -57,7 +57,7 @@
       in
         Pretty.big_list
           (msg ^ " could be solved directly with:")
-          (map (FindTheorems.pretty_thm ctxt) results)
+          (map (Find_Theorems.pretty_thm ctxt) results)
       end;
 
     fun seek_against_goal () =