diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml
index 488fae7c6f..99111f8fb2 100644
--- a/src/ecTheoryReplay.ml
+++ b/src/ecTheoryReplay.ml
@@ -75,9 +75,7 @@ let constr_compatible exn env cs1 cs2 =
 
 let datatype_compatible exn hyps ty1 ty2 =
   let env = EcEnv.LDecl.toenv hyps in
-  constr_compatible exn env ty1.tydt_ctors ty2.tydt_ctors;
-  error_body exn (EcReduction.is_conv hyps ty1.tydt_schcase ty2.tydt_schcase);
-  error_body exn (EcReduction.is_conv hyps ty1.tydt_schelim ty2.tydt_schelim)
+  constr_compatible exn env ty1.tydt_ctors ty2.tydt_ctors
 
 let record_compatible exn hyps f1 pr1 f2 pr2 =
   error_body exn (EcReduction.is_conv hyps f1 f2);
@@ -118,7 +116,6 @@ let tydecl_compatible env tyd1 tyd2 =
   | `Abstract _, _ -> () (* FIXME Sp.t *)
   | _, _ -> tybody_compatible exn hyps ty_body1 ty_body2
 
-
 (* -------------------------------------------------------------------- *)
 let expr_compatible exn env s e1 e2 =
   let f1 = EcFol.form_of_expr EcFol.mhr e1 in