# HG changeset patch
# User wenzelm
# Date 1288018340 -7200
# Node ID db6e84082695ce6bc9c2e2c9c2808425a110f8b7
# Parent  0843888de43e6b1b67971712840614119c12a1e6
export main ML entry by default;
observe elisp format for preferences;
clarified command setup;

diff -r 0843888de43e -r db6e84082695 src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Mon Oct 25 16:41:23 2010 +0200
+++ b/src/Tools/solve_direct.ML	Mon Oct 25 16:52:20 2010 +0200
@@ -10,12 +10,13 @@
 
 signature SOLVE_DIRECT =
 sig
-  val auto : bool Unsynchronized.ref
-  val max_solutions : int Unsynchronized.ref
-  val setup : theory -> theory
+  val auto: bool Unsynchronized.ref
+  val max_solutions: int Unsynchronized.ref
+  val solve_direct: bool -> Proof.state -> bool * Proof.state
+  val setup: theory -> theory
 end;
 
-structure Solve_Direct : SOLVE_DIRECT =
+structure Solve_Direct: SOLVE_DIRECT =
 struct
 
 val solve_directN = "solve_direct";
@@ -30,7 +31,7 @@
   ProofGeneralPgip.add_preference Preferences.category_tracing
   (Unsynchronized.setmp auto true (fn () =>
     Preferences.bool_pref auto
-      ("Auto " ^ solve_directN)
+      "auto-solve-direct"
       ("Run " ^ quote solve_directN ^ " automatically.")) ());
 
 
@@ -87,12 +88,11 @@
     | _ => (false, state))
   end;
 
-val invoke_solve_direct = fst o solve_direct false;
-
 val _ =
   Outer_Syntax.improper_command solve_directN
     "try to solve conjectures directly with existing theorems" Keyword.diag
-    (Scan.succeed (Toplevel.keep (K () o invoke_solve_direct o Toplevel.proof_of)));
+    (Scan.succeed
+      (Toplevel.keep (fn state => ignore (solve_direct false (Toplevel.proof_of state)))));
 
 
 (* hook *)