--- a/src/HOL/Proofs/Extraction/QuotRem.thy	Tue Jan 02 16:17:13 2018 +0100
+++ b/src/HOL/Proofs/Extraction/QuotRem.thy	Tue Jan 02 16:40:54 2018 +0100
@@ -5,7 +5,7 @@
 section \<open>Quotient and remainder\<close>
 
 theory QuotRem
-imports "HOL-Library.Old_Datatype" Util
+imports Util "HOL-Library.Realizers"
 begin
 
 text \<open>Derivation of quotient and remainder using program extraction.\<close>