# HG changeset patch
# User wenzelm
# Date 1274818346 -7200
# Node ID b36a5512c5fbe277af10bf6b3dcbc7885eaacab5
# Parent  ccae4ecd67f445a8c786c911f581ac9129455a5d
renamed HOLCF/Library/ROOT.ML to HOLCF/Library/HOLCF_Library_ROOT.ML to avoid accidental uses of this ML file via the load path -- see also d7711be8c3a9 (obsolete) and ccae4ecd67f4;

diff -r ccae4ecd67f4 -r b36a5512c5fb src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Tue May 25 21:49:44 2010 +0200
+++ b/src/HOLCF/IsaMakefile	Tue May 25 22:12:26 2010 +0200
@@ -101,8 +101,8 @@
   Library/Strict_Fun.thy \
   Library/Sum_Cpo.thy \
   Library/HOLCF_Library.thy \
-  Library/ROOT.ML
-	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library
+  Library/HOLCF_Library_ROOT.ML
+	@$(ISABELLE_TOOL) usedir -f HOLCF_Library_ROOT.ML $(OUT)/HOLCF Library
 
 
 ## HOLCF-IMP
diff -r ccae4ecd67f4 -r b36a5512c5fb src/HOLCF/Library/HOLCF_Library_ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Library/HOLCF_Library_ROOT.ML	Tue May 25 22:12:26 2010 +0200
@@ -0,0 +1,1 @@
+use_thys ["HOLCF_Library"];
diff -r ccae4ecd67f4 -r b36a5512c5fb src/HOLCF/Library/ROOT.ML
--- a/src/HOLCF/Library/ROOT.ML	Tue May 25 21:49:44 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-use_thys ["HOLCF_Library"];