diff -r 17414e2736f4 -r e03059ae2d82 src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Thu Jul 09 22:36:11 2009 +0200
+++ b/src/Pure/term_subst.ML	Thu Jul 09 22:48:12 2009 +0200
@@ -25,7 +25,7 @@
     ((indexname * sort) * typ) list * ((indexname * typ) * term) list
 end;
 
-structure TermSubst: TERM_SUBST =
+structure Term_Subst: TERM_SUBST =
 struct
 
 (* generalization of fixed variables *)