--- a/src/HOL/Tools/SMT/smtlib_interface.ML Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Fri Aug 27 10:56:46 2010 +0200
@@ -159,8 +159,8 @@
fun conn @{const_name True} = SOME "true"
| conn @{const_name False} = SOME "false"
| conn @{const_name Not} = SOME "not"
- | conn @{const_name "op &"} = SOME "and"
- | conn @{const_name "op |"} = SOME "or"
+ | 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 If} = SOME "if_then_else"