diff -r ff6d7206dd04 -r 8dd033c3ffbc Subst/ROOT.ML
--- a/Subst/ROOT.ML	Fri Oct 08 13:46:13 1993 +0100
+++ b/Subst/ROOT.ML	Sun Oct 17 17:23:51 1993 +0100
@@ -14,7 +14,7 @@
 setplus      -  minor additions to HOL's set theory
 alist        -  association lists
 uterm        -  inductive data type of terms
-utermlemmas  -  definition of occurs and vars_of for terms
+utlemmas     -  definition of occurs and vars_of for terms
 subst        -  substitutions
 unifier      -  specification of unification and conditions for 
                 correctness and termination
@@ -29,7 +29,7 @@
 
 use_thy "Subst/alist";
 use_thy "Subst/uterm";
-use_thy "Subst/utermlemmas";
+use_thy "Subst/utlemmas";
 
 use_thy "Subst/subst";
 use_thy "Subst/unifier";