--- a/src/HOL/Library/SCT_Implementation.thy	Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/Library/SCT_Implementation.thy	Fri Aug 24 14:14:20 2007 +0200
@@ -6,7 +6,7 @@
 header {* Implemtation of the SCT criterion *}
 
 theory SCT_Implementation
-imports Executable_Set SCT_Definition SCT_Theorem
+imports SCT_Definition SCT_Theorem
 begin
 
 fun edges_match :: "('n \<times> 'e \<times> 'n) \<times> ('n \<times> 'e \<times> 'n) \<Rightarrow> bool"