src/HOL/Tools/SMT/smtlib_interface.ML
changeset 38795 848be46708dc
parent 38786 e46e7a9cb622
child 38864 4abe644fcea5
--- 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"