src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
changeset 40059 6ad9081665db
parent 39975 7c50d5ca5c04
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Oct 21 14:54:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Oct 21 14:55:09 2010 +0200
@@ -16,7 +16,7 @@
   val prepare_axiom :
     Proof.context -> (string * 'a) * thm
     -> term * ((string * 'a) * fol_formula) option
-  val prepare_problem :
+  val prepare_atp_problem :
     Proof.context -> bool -> bool -> bool -> bool -> term list -> term
     -> (term * ((string * 'a) * fol_formula) option) list
     -> string problem * string Symtab.table * int * (string * 'a) list vector
@@ -494,8 +494,8 @@
   repair_problem_with_const_table thy explicit_forall full_types
       (const_table_for_problem explicit_apply problem) problem
 
-fun prepare_problem ctxt readable_names explicit_forall full_types
-                    explicit_apply hyp_ts concl_t axioms =
+fun prepare_atp_problem ctxt readable_names explicit_forall full_types
+                        explicit_apply hyp_ts concl_t axioms =
   let
     val thy = ProofContext.theory_of ctxt
     val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,