src/HOL/Metis_Examples/Tarski.thy

--- a/src/HOL/Metis_Examples/Tarski.thy	Tue May 15 06:23:12 2018 +0200
+++ b/src/HOL/Metis_Examples/Tarski.thy	Tue May 15 11:33:43 2018 +0200
@@ -8,7 +8,7 @@
 section \<open>Metis Example Featuring the Full Theorem of Tarski\<close>
 
 theory Tarski
-imports Main HOL.FuncSet
+imports Main "HOL-Library.FuncSet"
 begin
 
 declare [[metis_new_skolem]]