# HG changeset patch
# User wenzelm
# Date 1238531013 -7200
# Node ID 14d24e1fe594b061b05ed1160882a3ffd2e1558f
# Parent  bc6b24882834d8e7092cc0b7069a86e0d77c6d0e
fixed header;
misc simplification, use Conjunction.dest_conjunctions;

diff -r bc6b24882834 -r 14d24e1fe594 src/Tools/auto_solve.ML
--- a/src/Tools/auto_solve.ML	Tue Mar 31 21:31:23 2009 +0200
+++ b/src/Tools/auto_solve.ML	Tue Mar 31 22:23:33 2009 +0200
@@ -1,11 +1,11 @@
-(*  Title:      Pure/Tools/auto_solve.ML
+(*  Title:      Tools/auto_solve.ML
     Author:     Timothy Bourke and Gerwin Klein, NICTA
 
 Check whether a newly stated theorem can be solved directly by an
-existing theorem. Duplicate lemmas can be detected in this way.
+existing theorem.  Duplicate lemmas can be detected in this way.
 
-The implemenation is based in part on Berghofer and Haftmann's
-Pure/codegen.ML. It relies critically on the FindTheorems solves
+The implementation is based in part on Berghofer and Haftmann's
+quickcheck.ML.  It relies critically on the FindTheorems solves
 feature.
 *)
 
@@ -29,24 +29,15 @@
   let
     val ctxt = Proof.context_of state;
 
-    fun conj_to_list [] = []
-      | conj_to_list (t::ts) =
-        (Conjunction.dest_conjunction t
-         |> (fn (t1, t2) => conj_to_list (t1::t2::ts)))
-        handle TERM _ => t::conj_to_list ts;
-
     val crits = [(true, FindTheorems.Solves)];
-    fun find g = (NONE, snd (FindTheorems.find_theorems ctxt g (SOME (! limit)) false crits));
-    fun find_cterm g =
-      (SOME g, snd (FindTheorems.find_theorems ctxt
-          (SOME (Goal.init g)) (SOME (! limit)) false crits));
+    fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
 
     fun prt_result (goal, results) =
       let
         val msg =
           (case goal of
             NONE => "The current goal"
-          | SOME g => Syntax.string_of_term ctxt (Thm.term_of g));
+          | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
       in
         Pretty.big_list
           (msg ^ " could be solved directly with:")
@@ -54,22 +45,17 @@
       end;
 
     fun seek_against_goal () =
-      let
-        val goal = try Proof.get_goal state
-          |> Option.map (#2 o #2);
-
-        val goals = goal
-          |> Option.map (fn g => cprem_of g 1)
-          |> the_list
-          |> conj_to_list;
-
-        val rs =
-          if length goals = 1
-          then [find goal]
-          else map find_cterm goals;
-        val results = filter_out (null o snd) rs;
-
-      in if null results then NONE else SOME results end;
+      (case try Proof.get_goal state of
+        NONE => NONE
+      | SOME (_, (_, goal)) =>
+          let
+            val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
+            val rs =
+              if length subgoals = 1
+              then [(NONE, find goal)]
+              else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
+            val results = filter_out (null o snd) rs;
+          in if null results then NONE else SOME results end);
 
     fun go () =
       let
@@ -84,7 +70,7 @@
                 [Pretty.str "",
                   Pretty.markup Markup.hilite
                     (separate (Pretty.brk 0) (map prt_result results))])
-        | NONE => state)
+        | _ => state)
       end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
   in
     if int andalso ! auto andalso not (! Toplevel.quiet)