--- 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 () =