regular image setup for HOL-Library (cf. 4915de09b4d3 and ccae4ecd67f4) -- note that document preparation requires a separate session directory, and library.ML is a bit too generic as a file in the default load path;

--- a/src/HOL/IsaMakefile	Sat Jul 10 21:38:16 2010 +0200
+++ b/src/HOL/IsaMakefile	Sat Jul 10 22:39:16 2010 +0200
@@ -395,7 +395,7 @@
 
 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			\
@@ -437,7 +437,7 @@
   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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/HOL_Library_ROOT.ML	Sat Jul 10 22:39:16 2010 +0200
@@ -0,0 +1,5 @@
+
+(* Classical Higher-order Logic -- batteries included *)
+
+use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
+  "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set"];

--- a/src/HOL/library.ML	Sat Jul 10 21:38:16 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-
-(* Classical Higher-order Logic -- batteries included *)
-
-use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
-  "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set"];