1.1 --- a/src/HOL/Tools/res_atp.ML	Sat Aug 18 13:32:20 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Sat Aug 18 13:32:21 2007 +0200
     1.3 @@ -17,8 +17,6 @@
     1.4    datatype mode = Auto | Fol | Hol
     1.5    val linkup_logic_mode : mode ref
     1.6    val write_subgoal_file: bool -> mode -> Proof.context -> thm list -> thm list -> int -> string
     1.7 -  val atp_method: (Proof.context -> thm list -> int -> tactic) ->
     1.8 -    Method.src -> Proof.context -> Proof.method
     1.9    val cond_rm_tmp: string -> unit
    1.10    val include_all: bool ref
    1.11    val run_relevance_filter: bool ref
    1.12 @@ -762,9 +760,9 @@
    1.13    likely to lead to unsound proofs.*)
    1.14  fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
    1.15  
    1.16 -fun tptp_writer logic = ResHolClause.tptp_write_file (logic=FOL);
    1.17 +fun tptp_writer thy logic = ResHolClause.tptp_write_file thy (logic=FOL);
    1.18  
    1.19 -fun dfg_writer logic = ResHolClause.dfg_write_file (logic=FOL);
    1.20 +fun dfg_writer thy logic = ResHolClause.dfg_write_file thy (logic=FOL);
    1.21  
    1.22  (*Called by the oracle-based methods declared in res_atp_methods.ML*)
    1.23  fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
    1.24 @@ -796,7 +794,7 @@
    1.25          and file = atp_input_file()
    1.26          and user_lemmas_names = map #1 user_rules
    1.27      in
    1.28 -        writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
    1.29 +        writer thy logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
    1.30          Output.debug (fn () => "Writing to " ^ file);
    1.31          file
    1.32      end;
    1.33 @@ -809,16 +807,6 @@
    1.34      else OS.FileSys.remove file;
    1.35  
    1.36  
    1.37 -(****** setup ATPs as Isabelle methods ******)
    1.38 -
    1.39 -fun atp_meth tac ths ctxt =
    1.40 -    let val thy = ProofContext.theory_of ctxt
    1.41 -        val _ = ResClause.init thy
    1.42 -        val _ = ResHolClause.init thy
    1.43 -    in Method.SIMPLE_METHOD' (tac ctxt ths) end;
    1.44 -
    1.45 -fun atp_method tac = Method.thms_ctxt_args (atp_meth tac);
    1.46 -
    1.47  (***************************************************************)
    1.48  (* automatic ATP invocation                                    *)
    1.49  (***************************************************************)
    1.50 @@ -918,7 +906,7 @@
    1.51                  val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses))
    1.52                  val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
    1.53                  val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses))
    1.54 -                val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
    1.55 +                val clnames = writer thy logic ccls fname (axcls,classrel_clauses,arity_clauses) []
    1.56                  val thm_names = Vector.fromList clnames
    1.57                  val _ = if !Output.debugging then trace_vector fname thm_names else ()
    1.58              in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
    1.59 @@ -980,8 +968,6 @@
    1.60                    Pretty.string_of (ProofContext.pretty_term ctxt
    1.61                      (Logic.mk_conjunction_list (Thm.prems_of goal))));
    1.62      Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
    1.63 -    ResClause.init thy;
    1.64 -    ResHolClause.init thy;
    1.65      if !time_limit > 0 then isar_atp (ctxt, goal)
    1.66      else (warning ("Writing problem file only: " ^ !problem_name);
    1.67            isar_atp_writeonly (ctxt, goal))