diff --git a/src/smtencoding/FStar.SMTEncoding.Solver.fst b/src/smtencoding/FStar.SMTEncoding.Solver.fst
index 7d9bf011777..bc1350b8e9a 100644
--- a/src/smtencoding/FStar.SMTEncoding.Solver.fst
+++ b/src/smtencoding/FStar.SMTEncoding.Solver.fst
@@ -48,10 +48,6 @@ exception SplitQueryAndRetry
 // The type definition is now in [FStar.Compiler.Util], since it needs to be visible to
 // both the F# and OCaml implementations.
 
-type z3_replay_result = either Z3.unsat_core, error_labels
-let z3_result_as_replay_result = function
-    | Inl l -> Inl l
-    | Inr (r, _) -> Inr r
 let recorded_hints : ref (option hints) = BU.mk_ref None
 let replaying_hints: ref (option hints) = BU.mk_ref None