diff -r 1f5497c8ce8c -r 8a9f0503b1c0 src/HOL/IMP/Abs_Int_init.thy
--- a/src/HOL/IMP/Abs_Int_init.thy	Sun Mar 10 14:36:18 2013 +0100
+++ b/src/HOL/IMP/Abs_Int_init.thy	Sun Mar 10 18:29:10 2013 +0100
@@ -1,6 +1,5 @@
 theory Abs_Int_init
-imports "~~/src/HOL/ex/Interpretation_with_Defs"
-        "~~/src/HOL/Library/While_Combinator"
+imports "~~/src/HOL/Library/While_Combinator"
         Vars Collecting Abs_Int_Tests
 begin