--- a/src/HOL/Quotient_Examples/ROOT.ML Wed Apr 28 17:42:37 2010 +0200
+++ b/src/HOL/Quotient_Examples/ROOT.ML Thu Apr 29 09:06:35 2010 +0200
@@ -4,5 +4,5 @@
Testing the quotient package.
*)
-use_thys ["FSet", "LarryInt", "LarryDatatype"];
+use_thys ["FSet", "Quotient_Int", "Quotient_Message"];