# HG changeset patch
# User huffman
# Date 1266525369 28800
# Node ID 67689d276c70a375215430b9174e3be6fbe6153f
# Parent  b9866ad4e3be229a5744394c9221f38d62fee961
HOLCF-FOCUS depends on ex/Stream.thy

diff -r b9866ad4e3be -r 67689d276c70 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Thu Feb 18 08:08:51 2010 -0800
+++ b/src/HOLCF/IsaMakefile	Thu Feb 18 12:36:09 2010 -0800
@@ -113,7 +113,9 @@
 
 HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
 
-$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF FOCUS/Fstreams.thy \
+$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF \
+  ex/Stream.thy \
+  FOCUS/Fstreams.thy \
   FOCUS/Fstream.thy FOCUS/FOCUS.thy \
   FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \
   FOCUS/Buffer.thy FOCUS/Buffer_adm.thy