1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Fri May 27 10:30:07 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri May 27 10:30:07 2011 +0200
     1.3 @@ -378,7 +378,7 @@
     1.4    let
     1.5      fun do_term_pair _ NONE = NONE
     1.6        | do_term_pair (ATerm (s1, tm1), ATerm (s2, tm2)) (SOME subst) =
     1.7 -        case pairself is_atp_variable (s1, s2) of
     1.8 +        case pairself is_tptp_variable (s1, s2) of
     1.9            (true, true) =>
    1.10            (case AList.lookup (op =) subst s1 of
    1.11               SOME s2' => if s2' = s2 then SOME subst else NONE