--- a/src/HOL/ex/ROOT.ML Tue Aug 03 13:15:36 1999 +0200
+++ b/src/HOL/ex/ROOT.ML Tue Aug 03 13:15:54 1999 +0200
@@ -33,6 +33,7 @@
time_use_thy "StringEx";
time_use_thy "BinEx";
+time_use "svc_test.ML";
(*basic use of extensible records*)
time_use_thy "MonoidGroup";