src/HOL/IsaMakefile

 
 ## HOL-Library
 
 HOL-Library: HOL $(OUT)/HOL-Library
 
-$(OUT)/HOL-Library: $(OUT)/HOL library.ML				\
+$(OUT)/HOL-Library: $(OUT)/HOL Library/HOL_Library_ROOT.ML		\
   $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML			\
   Library/Abstract_Rat.thy Library/AssocList.thy			\
   Library/BigO.thy Library/Binomial.thy Library/Bit.thy			\
   Library/Boolean_Algebra.thy Library/Cardinality.thy			\
   Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\

   Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
   Library/While_Combinator.thy Library/Zorn.thy				\
   Library/positivstellensatz.ML Library/reflection.ML			\
   Library/reify_data.ML							\
   Library/document/root.bib Library/document/root.tex
-	@$(ISABELLE_TOOL) usedir -b -f library.ML $(OUT)/HOL HOL-Library
+	@cd Library; $(ISABELLE_TOOL) usedir -b -f HOL_Library_ROOT.ML $(OUT)/HOL HOL-Library
 
 
 ## HOL-Hahn_Banach
 
 HOL-Hahn_Banach: HOL $(LOG)/HOL-Hahn_Banach.gz