# HG changeset patch
# User bulwahn
# Date 1290418915 -3600
# Node ID 47004929bc71cc1e62c37926313ceb1f4bf522c6
# Parent  dc124a486f94e06713352a7bce7b93926f8016a6
ported sledgehammer_tactic to current development version

diff -r dc124a486f94 -r 47004929bc71 src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Mon Nov 22 10:41:54 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Mon Nov 22 10:41:55 2010 +0100
@@ -21,8 +21,8 @@
       ((if force_full_types then [("full_types", "true")] else [])
        @ [("timeout", Int.toString (Time.toMilliseconds timeout) ^ " ms")])
 (*      @ [("overlord", "true")] *)
-      |> Sledgehammer_Isar.default_params thy
-    val prover = Sledgehammer.get_prover_fun thy name
+      |> Sledgehammer_Isar.default_params ctxt
+    val prover = Sledgehammer.get_prover thy false name
     val facts = []
     (* Check for constants other than the built-in HOL constants. If none of
        them appear (as should be the case for TPTP problems, unless "auto" or
@@ -32,8 +32,8 @@
                                       not (String.isSubstring "HOL" s))
                         (prop_of goal))
     val problem =
-      {state = Proof.init ctxt, goal = goal, subgoal = i, axioms = [],
-       only = true}
+      {state = Proof.init ctxt, goal = goal, subgoal = i, facts = [],
+       only = true, subgoal_count = n}
   in
     prover params (K "") problem |> #message
     handle ERROR message => "Error: " ^ message ^ "\n"
@@ -47,7 +47,7 @@
 val extract_metis_facts =
   space_explode " "
   #> fold (maps o space_explode) ["(", ")", Symbol.ENQ, Symbol.ACK, "\n"]
-  #> Library.dropwhile (not o member (op =) ["metis", "metisFT"])
+  #> fst o chop_while (not o member (op =) ["metis", "metisFT"])
   #> (fn _ :: ss => SOME (to_period ss) | _ => NONE)
 
 val atp = "e" (* or "vampire" *)
@@ -58,7 +58,7 @@
     val get = maps (ProofContext.get_fact ctxt o fst)
   in
     Source.of_string name
-    |> Symbol.source {do_recover=false}
+    |> Symbol.source
     |> Token.source {do_recover=SOME false} lex Position.start
     |> Token.source_proper
     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE