--- a/src/HOL/Tools/SMT/smtlib_interface.ML Sat Aug 28 20:24:40 2010 +0800
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Sat Aug 28 16:14:32 2010 +0200
@@ -162,12 +162,12 @@
| conn @{const_name HOL.conj} = SOME "and"
| conn @{const_name HOL.disj} = SOME "or"
| conn @{const_name HOL.implies} = SOME "implies"
- | conn @{const_name "op ="} = SOME "iff"
+ | conn @{const_name HOL.eq} = SOME "iff"
| conn @{const_name If} = SOME "if_then_else"
| conn _ = NONE
fun pred @{const_name distinct} _ = SOME "distinct"
- | pred @{const_name "op ="} _ = SOME "="
+ | pred @{const_name HOL.eq} _ = SOME "="
| pred @{const_name term_eq} _ = SOME "="
| pred @{const_name less} T = if_int_type T "<"
| pred @{const_name less_eq} T = if_int_type T "<="