src/HOL/Induct/ROOT.ML
changeset 33688 1a97dcd8dc6a
parent 33615 261abc2e3155
child 35247 0831bd85eee5
--- a/src/HOL/Induct/ROOT.ML	Sat Nov 14 18:45:24 2009 +0100
+++ b/src/HOL/Induct/ROOT.ML	Sat Nov 14 19:56:18 2009 +0100
@@ -2,5 +2,4 @@
   use_thys ["Common_Patterns"];
 
 use_thys ["QuoDataType", "QuoNestedDataType", "Term",
-  "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog",
-  "SList", "LFilter", "Com"];
+  "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog", "Com"];