1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Jul 05 17:09:59 2011 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Jul 05 17:09:59 2011 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  signature ATP_PROOF =
     1.6  sig
     1.7 -  type 'a fo_term = 'a ATP_Problem.fo_term
     1.8 +  type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
     1.9    type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
    1.10    type 'a problem = 'a ATP_Problem.problem
    1.11  
    1.12 @@ -41,7 +41,7 @@
    1.13      Definition of step_name * 'a * 'a |
    1.14      Inference of step_name * 'a * step_name list
    1.15  
    1.16 -  type 'a proof = ('a, 'a, 'a fo_term) formula step list
    1.17 +  type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
    1.18  
    1.19    val short_output : bool -> string -> string
    1.20    val string_for_failure : failure -> string
    1.21 @@ -54,7 +54,7 @@
    1.22    val is_same_atp_step : step_name -> step_name -> bool
    1.23    val scan_general_id : string list -> string * string list
    1.24    val parse_formula :
    1.25 -    string list -> (string, 'a, string fo_term) formula * string list
    1.26 +    string list -> (string, 'a, (string, 'a) ho_term) formula * string list
    1.27    val atp_proof_from_tstplike_proof :
    1.28      string problem -> string -> string -> string proof
    1.29    val clean_up_atp_proof_dependencies : string proof -> string proof
    1.30 @@ -228,7 +228,7 @@
    1.31    Definition of step_name * 'a * 'a |
    1.32    Inference of step_name * 'a * step_name list
    1.33  
    1.34 -type 'a proof = ('a, 'a, 'a fo_term) formula step list
    1.35 +type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
    1.36  
    1.37  fun step_name (Definition (name, _, _)) = name
    1.38    | step_name (Inference (name, _, _)) = name
    1.39 @@ -293,7 +293,7 @@
    1.40          | (u1, SOME (SOME _, u2)) =>
    1.41            mk_anot (AAtom (ATerm ("equal", [u1, u2]))))) x
    1.42  
    1.43 -fun fo_term_head (ATerm (s, _)) = s
    1.44 +fun ho_term_head (ATerm (s, _)) = s
    1.45  
    1.46  (* TPTP formulas are fully parenthesized, so we don't need to worry about
    1.47     operator precedence. *)
    1.48 @@ -325,7 +325,7 @@
    1.49     --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal
    1.50     >> (fn ((q, ts), phi) =>
    1.51            (* We ignore TFF and THF types for now. *)
    1.52 -          AQuant (q, map (rpair NONE o fo_term_head) ts, phi))) x
    1.53 +          AQuant (q, map (rpair NONE o ho_term_head) ts, phi))) x
    1.54  
    1.55  fun skip_formula ss =
    1.56    let