neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
external_prover: neg_conjecture_clauses should handle TVars within goals;
misc tuning;

--- a/src/HOL/Tools/atp_wrapper.ML	Tue Jul 28 18:17:35 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML	Tue Jul 28 18:17:35 2009 +0200
@@ -59,9 +59,7 @@
     val (ctxt, (chain_ths, th)) = goal
     val thy = ProofContext.theory_of ctxt
     val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
-    val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno)
-      handle THM ("assume: variables", _, _) =>
-        error "Sledgehammer: Goal contains type variables (TVars)"
+    val goal_cls = #1 (ResAxioms.neg_conjecture_clauses ctxt th subgoalno)
     val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm ctxt th)) goal_cls
     val the_filtered_clauses =
       case filtered_clauses of
@@ -71,7 +69,8 @@
       case axiom_clauses of
           NONE => the_filtered_clauses
         | SOME axcls => axcls
-    val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
+    val (thm_names, clauses) =
+      preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
 
     (* write out problem file and call prover *)
     val probfile = prob_pathname subgoalno
@@ -85,7 +84,7 @@
     val _ =
       if destdir' = "" then File.rm probfile
       else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
-    
+
     (* check for success and print out some information on failure *)
     val failure = find_failure proof
     val success = rc = 0 andalso is_none failure
@@ -133,7 +132,7 @@
 fun vampire_opts max_new theory_const timeout = tptp_prover_opts
   max_new theory_const
   (Path.explode "$VAMPIRE_HOME/vampire",
-               ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
+    ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
   timeout;
 
 val vampire = vampire_opts 60 false;
@@ -141,7 +140,7 @@
 fun vampire_opts_full max_new theory_const timeout = full_prover_opts
   max_new theory_const
   (Path.explode "$VAMPIRE_HOME/vampire",
-               ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
+    ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
   timeout;
 
 val vampire_full = vampire_opts_full 60 false;
@@ -173,7 +172,8 @@
   (ResAtp.prepare_clauses true)
   (ResHolClause.dfg_write_file (AtpManager.get_full_types()))
   (Path.explode "$SPASS_HOME/SPASS",
-    "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
+    "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^
+      string_of_int timeout)
   ResReconstruct.find_failure
   (ResReconstruct.lemma_list true)
   timeout ax_clauses fcls name n goal;
@@ -196,22 +196,23 @@
   end;
 
 fun refresh_systems () = Synchronized.change systems (fn _ =>
-  get_systems());
+  get_systems ());
 
 fun get_system prefix = Synchronized.change_result systems (fn systems =>
   let val systems = if null systems then get_systems() else systems
   in (find_first (String.isPrefix prefix) systems, systems) end);
 
 fun remote_prover_opts max_new theory_const args prover_prefix timeout =
-  let val sys = case get_system prover_prefix of
+  let val sys =
+    case get_system prover_prefix of
       NONE => error ("No system like " ^ quote prover_prefix ^ " at SystemOnTPTP")
     | SOME sys => sys
   in tptp_prover_opts max_new theory_const
     (Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP",
-      args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout end;
+      args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout
+  end;
 
 val remote_prover = remote_prover_opts 60 false;
 
 end;
 
-

--- a/src/HOL/Tools/res_axioms.ML	Tue Jul 28 18:17:35 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Tue Jul 28 18:17:35 2009 +0200
@@ -14,7 +14,7 @@
   val neg_clausify: thm list -> thm list
   val expand_defs_tac: thm -> tactic
   val combinators: thm -> thm
-  val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
+  val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list
   val atpset_rules_of: Proof.context -> (string * thm) list
   val suppress_endtheory: bool ref     (*for emergency use where endtheory causes problems*)
   val setup: theory -> theory
@@ -498,32 +498,30 @@
 
 val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac];
 
-fun neg_clausify sts =
-  sts |> Meson.make_clauses |> map combinators |> Meson.finish_cnf;
+val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
 
-fun neg_conjecture_clauses st0 n =
-  let val st = Seq.hd (neg_skolemize_tac n st0)
-      val (params,_,_) = OldGoals.strip_context (Logic.nth_prem (n, Thm.prop_of st))
-  in (neg_clausify (the (OldGoals.metahyps_thms n st)), params) end
-  handle Option => error "unable to Skolemize subgoal";
+fun neg_conjecture_clauses ctxt st0 n =
+  let
+    val st = Seq.hd (neg_skolemize_tac n st0)
+    val ({params, prems, ...}, _) = Subgoal.focus (Variable.set_body false ctxt) n st
+  in (neg_clausify prems, map (Term.dest_Free o Thm.term_of o #2) params) end;
 
 (*Conversion of a subgoal to conjecture clauses. Each clause has
   leading !!-bound universal variables, to express generality. *)
-val neg_clausify_tac =
+fun neg_clausify_tac ctxt =
   neg_skolemize_tac THEN'
-  SUBGOAL
-    (fn (prop,_) =>
-     let val ts = Logic.strip_assums_hyp prop
-     in EVERY1
-         [OldGoals.METAHYPS
-            (fn hyps =>
-              (Method.insert_tac
-                (map forall_intr_vars (neg_clausify hyps)) 1)),
-          REPEAT_DETERM_N (length ts) o (etac thin_rl)]
+  SUBGOAL (fn (prop, i) =>
+    let val ts = Logic.strip_assums_hyp prop in
+      EVERY'
+       [FOCUS
+         (fn {prems, ...} =>
+           (Method.insert_tac
+             (map forall_intr_vars (neg_clausify prems)) i)) ctxt,
+        REPEAT_DETERM_N (length ts) o etac thin_rl] i
      end);
 
 val neg_clausify_setup =
-  Method.setup @{binding neg_clausify} (Scan.succeed (K (SIMPLE_METHOD' neg_clausify_tac)))
+  Method.setup @{binding neg_clausify} (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac))
   "conversion of goal to conjecture clauses";