src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
changeset 38864 4abe644fcea5
parent 38829 c18e8f90f4dc
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -315,7 +315,7 @@
     1.4            | _ => raise FO_TERM us
     1.5          else case strip_prefix_and_unascii const_prefix a of
     1.6            SOME "equal" =>
     1.7 -          list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
     1.8 +          list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT),
     1.9                       map (aux NONE []) us)
    1.10          | SOME b =>
    1.11            let
    1.12 @@ -527,7 +527,7 @@
    1.13    | is_bad_free _ _ = false
    1.14  
    1.15  (* Vampire is keen on producing these. *)
    1.16 -fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _)
    1.17 +fun is_trivial_formula (@{const Not} $ (Const (@{const_name HOL.eq}, _)
    1.18                                          $ t1 $ t2)) = (t1 aconv t2)
    1.19    | is_trivial_formula _ = false
    1.20