Optimization hack for checking operator compatibility in clones

The conversion check has a strategy to unfold the LHS before the RHS
when checking that two maybe applied different operators are
convertible. When cloning a theory with the "theory T <- U"
stanza, the RHS of the conversion is an alias to the RHS. By
swapping the two arguments, the convertibility check is immediate,
while on the other case, both hands will be normalized.

A proper way to solve this problem would be to have a more
advanced unfold heuristic (by using a generation ID per operators
or having more meta-information on the operators bodies)

Author: strub

src/ecTheoryReplay.ml

@@ -237,10 +237,10 @@ let operator_compatible env oper1 oper2 =
   let exn  = Incompatible (OpBody(*oper1,oper2*)) in
   match okind1, okind2 with
   | OB_oper None      , OB_oper _          -> ()
-  | OB_oper (Some ob1), OB_oper (Some ob2) -> oper_compatible exn env ob1 ob2
+  | OB_oper (Some ob1), OB_oper (Some ob2) -> oper_compatible exn env ob2 ob1
   | OB_pred None      , OB_pred _          -> ()
-  | OB_pred (Some pb1), OB_pred (Some pb2) -> pred_compatible exn env pb1 pb2
-  | OB_nott nb1       , OB_nott nb2        -> nott_compatible exn env nb1 nb2
+  | OB_pred (Some pb1), OB_pred (Some pb2) -> pred_compatible exn env pb2 pb1
+  | OB_nott nb1       , OB_nott nb2        -> nott_compatible exn env nb2 nb1
   | _                 , _                  -> raise exn
 
 (* -------------------------------------------------------------------- *)