diff -r 8dd033c3ffbc -r da00b32c3977 ex/ROOT.ML
--- a/ex/ROOT.ML	Sun Oct 17 17:23:51 1993 +0100
+++ b/ex/ROOT.ML	Sun Oct 17 17:33:40 1993 +0100
@@ -1,4 +1,4 @@
-(*  Title: 	HOL/ex/ROOT
+(*  Title:  	HOL/ex/ROOT
     ID:         $Id$
     Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
@@ -13,11 +13,11 @@
 time_use     "ex/cla.ML";
 time_use     "ex/meson.ML";
 time_use     "ex/meson-test.ML";
-time_use_thy "ex/lex-prod";
+time_use_thy "ex/lexprod";
 time_use_thy "ex/puzzle";
 time_use     "ex/set.ML";
 time_use_thy "ex/finite";
-time_use_thy "ex/prop-log";
+time_use_thy "ex/pl";
 time_use_thy "ex/term";
 time_use_thy "ex/simult";
 maketest     "END: Root file for HOL examples";