diff -r 11fca474d87a -r b1278ed3cd46 src/HOL/ex/PresburgerEx.thy
--- a/src/HOL/ex/PresburgerEx.thy	Sat Nov 04 18:57:49 2017 +0100
+++ b/src/HOL/ex/PresburgerEx.thy	Sat Nov 04 19:17:19 2017 +0100
@@ -5,7 +5,7 @@
 section \<open>Some examples for Presburger Arithmetic\<close>
 
 theory PresburgerEx
-imports HOL.Presburger
+imports Main
 begin
 
 lemma "\<And>m n ja ia. \<lbrakk>\<not> m \<le> j; \<not> (n::nat) \<le> i; (e::nat) \<noteq> 0; Suc j \<le> ja\<rbrakk> \<Longrightarrow> \<exists>m. \<forall>ja ia. m \<le> ja \<longrightarrow> (if j = ja \<and> i = ia then e else 0) = 0" by presburger