diff -r e865dda0313e -r f171fa6a0989 src/FOL/ex/ROOT.ML
--- a/src/FOL/ex/ROOT.ML	Thu Jun 29 22:39:57 2000 +0200
+++ b/src/FOL/ex/ROOT.ML	Thu Jun 29 22:48:08 2000 +0200
@@ -12,7 +12,7 @@
 time_use_thy "Prolog";
 
 writeln"\n** Intuitionistic examples **\n";
-time_use     "int.ML";
+time_use_thy "int";
 
 val thy = IFOL.thy  and  tac = IntPr.fast_tac 1;
 time_use     "prop.ML";