1.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Feb 03 14:35:19 2014 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Feb 03 15:19:07 2014 +0100
     1.3 @@ -28,9 +28,9 @@
     1.4    val partial_type_encs : string list
     1.5    val default_metis_lam_trans : string
     1.6  
     1.7 -  val metis_call : string -> string -> string
     1.8    val forall_of : term -> term -> term
     1.9    val exists_of : term -> term -> term
    1.10 +  val type_enc_aliases : (string * string list) list
    1.11    val unalias_type_enc : string -> string list
    1.12    val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option ->
    1.13      (string, string atp_type) atp_term -> term
    1.14 @@ -84,17 +84,6 @@
    1.15  
    1.16  val default_metis_lam_trans = combsN
    1.17  
    1.18 -fun metis_call type_enc lam_trans =
    1.19 -  let
    1.20 -    val type_enc =
    1.21 -      (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
    1.22 -        [alias] => alias
    1.23 -      | _ => type_enc)
    1.24 -    val opts =
    1.25 -      [] |> type_enc <> partial_typesN ? cons type_enc
    1.26 -         |> lam_trans <> default_metis_lam_trans ? cons lam_trans
    1.27 -  in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
    1.28 -
    1.29  fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s
    1.30    | term_name' _ = ""
    1.31