src/HOL/Number_Theory/Prime_Powers.thy

--- a/src/HOL/Number_Theory/Prime_Powers.thy	Wed Apr 18 21:12:50 2018 +0100
+++ b/src/HOL/Number_Theory/Prime_Powers.thy	Wed May 02 13:49:38 2018 +0200
@@ -6,7 +6,7 @@
 *)
 section \<open>Prime powers\<close>
 theory Prime_Powers
-  imports Complex_Main "HOL-Computational_Algebra.Primes" "HOL-Library.FuncSet"
+  imports Complex_Main "HOL-Computational_Algebra.Primes"
 begin
 
 definition aprimedivisor :: "'a :: normalization_semidom \<Rightarrow> 'a" where