1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 01 10:29:43 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 01 10:29:43 2011 +0200
     1.3 @@ -9,6 +9,8 @@
     1.4  signature ATP_TRANSLATE =
     1.5  sig
     1.6    type 'a fo_term = 'a ATP_Problem.fo_term
     1.7 +  type connective = ATP_Problem.connective
     1.8 +  type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
     1.9    type format = ATP_Problem.format
    1.10    type formula_kind = ATP_Problem.formula_kind
    1.11    type 'a problem = 'a ATP_Problem.problem
    1.12 @@ -115,6 +117,8 @@
    1.13    val is_type_sys_fairly_sound : type_sys -> bool
    1.14    val choose_format : format list -> type_sys -> format * type_sys
    1.15    val raw_type_literals_for_types : typ list -> type_literal list
    1.16 +  val mk_aconns :
    1.17 +    connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
    1.18    val unmangled_const_name : string -> string
    1.19    val unmangled_const : string -> string * string fo_term list
    1.20    val translate_atp_fact :