src/HOL/Tools/SMT/z3_proof_literals.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 40579 98ebd2300823
     1.1 --- a/src/HOL/Tools/SMT/z3_proof_literals.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_literals.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -234,7 +234,7 @@
     1.4          @{term Not} $ (@{term Not} $ t) => (T.compose dnegI, lookup t)
     1.5        | @{term Not} $ (@{term "op = :: bool => _"} $ t $ (@{term Not} $ u)) =>
     1.6            (T.compose negIffI, lookup (iff_const $ u $ t))
     1.7 -      | @{term Not} $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u) =>
     1.8 +      | @{term Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
     1.9            let fun rewr lit = lit COMP @{thm not_sym}
    1.10            in (rewr, lookup (@{term Not} $ (eq $ u $ t))) end
    1.11        | _ =>