src/Tools/Metis/src/Clause.sml

--- a/src/Tools/Metis/src/Clause.sml	Tue Nov 13 17:04:16 2007 +0100
+++ b/src/Tools/Metis/src/Clause.sml	Tue Nov 13 18:29:28 2007 +0100
@@ -95,8 +95,9 @@
 
 local
   fun atomToTerms atm =
-      Term.Fn atm ::
-      (case total Atom.sym atm of NONE => [] | SOME atm => [Term.Fn atm]);
+      case total Atom.destEq atm of
+        NONE => [Term.Fn atm]
+      | SOME (l,r) => [l,r];
 
   fun notStrictlyLess ordering (xs,ys) =
       let