--- a/src/HOL/Proofs/Extraction/Util.thy Thu Sep 18 16:47:40 2014 +0200
+++ b/src/HOL/Proofs/Extraction/Util.thy Thu Sep 18 16:47:40 2014 +0200
@@ -5,7 +5,7 @@
header {* Auxiliary lemmas used in program extraction examples *}
theory Util
-imports Main
+imports Old_Datatype
begin
text {*