--- a/src/HOL/Quotient_Examples/ROOT.ML Thu Apr 22 22:12:12 2010 +0200
+++ b/src/HOL/Quotient_Examples/ROOT.ML Fri Apr 23 10:00:53 2010 +0200
@@ -4,5 +4,5 @@
Testing the quotient package.
*)
-use_thys ["LarryInt", "LarryDatatype"];
+use_thys ["FSet", "LarryInt", "LarryDatatype"];