src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
changeset 38007 f0a4aa17f23f
parent 37998 f1b7fb87f523
child 38014 81c23d286f0c
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Jul 27 00:08:05 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Jul 27 12:01:02 2010 +0200
     1.3 @@ -73,7 +73,7 @@
     1.4  (* needed for SPASS's output format *)
     1.5  fun repair_name _ "$true" = "c_True"
     1.6    | repair_name _ "$false" = "c_False"
     1.7 -  | repair_name _ "$$e" = "c_equal" (* seen in Vampire 11 proofs *)
     1.8 +  | repair_name _ "$$e" = "c_equal" (* seen in Vampire proofs *)
     1.9    | repair_name _ "equal" = "c_equal" (* probably not needed *)
    1.10    | repair_name pool s = Symtab.lookup pool s |> the_default s
    1.11  (* Generalized first-order terms, which include file names, numbers, etc. *)
    1.12 @@ -142,7 +142,10 @@
    1.13             case role of
    1.14               "definition" =>
    1.15               (case phi of
    1.16 -                AConn (AIff, [phi1, phi2]) => Definition (num, phi1, phi2)
    1.17 +                AConn (AIff, [phi1 as APred _, phi2]) =>
    1.18 +                Definition (num, phi1, phi2)
    1.19 +              | APred (ATerm ("$$e", _)) =>
    1.20 +                Inference (num, phi, deps) (* Vampire's equality proxy axiom *)
    1.21                | _ => raise Fail "malformed definition")
    1.22             | _ => Inference (num, phi, deps))
    1.23