--- a/src/Tools/solve_direct.ML Thu Jul 18 21:57:27 2013 +0200
+++ b/src/Tools/solve_direct.ML Thu Jul 18 22:00:35 2013 +0200
@@ -29,6 +29,7 @@
val noneN = "none";
val unknownN = "none";
+
(* preferences *)
val max_solutions = Unsynchronized.ref 5;
@@ -46,10 +47,11 @@
fun do_solve_direct mode state =
let
val ctxt = Proof.context_of state;
+ val find_ctxt = if mode = Auto_Try then Context_Position.set_visible false ctxt else ctxt;
val crits = [(true, Find_Theorems.Solves)];
fun find g =
- snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits);
+ snd (Find_Theorems.find_theorems find_ctxt (SOME g) (SOME (! max_solutions)) false crits);
fun prt_result (goal, results) =
let