1.1 --- a/src/HOL/Tools/atp_wrapper.ML	Mon Jun 22 17:07:08 2009 +0200
     1.2 +++ b/src/HOL/Tools/atp_wrapper.ML	Mon Jun 22 17:07:08 2009 +0200
     1.3 @@ -54,12 +54,10 @@
     1.4          else error ("No such directory: " ^ destdir')
     1.5        end
     1.6  
     1.7 -    (* write out problem file and call prover *)
     1.8 +    (* get clauses and prepare them for writing *)
     1.9      val (ctxt, (chain_ths, th)) = goal
    1.10      val thy = ProofContext.theory_of ctxt
    1.11      val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
    1.12 -    val probfile = prob_pathname subgoalno
    1.13 -    val fname = File.platform_path probfile
    1.14      val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno)
    1.15        handle THM ("assume: variables", _, _) =>
    1.16          error "Sledgehammer: Goal contains type variables (TVars)"
    1.17 @@ -77,6 +75,10 @@
    1.18              | SOME axcls => #2(preparer goal_cls chain_ths (relevance_filter goal goal_cls) thy)
    1.19            )
    1.20        | SOME ccs => ccs
    1.21 +
    1.22 +    (* write out problem file and call prover *)
    1.23 +    val probfile = prob_pathname subgoalno
    1.24 +    val fname = File.platform_path probfile
    1.25      val _ = writer fname the_const_counts clauses
    1.26      val cmdline =
    1.27        if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args