diff -r 0b05cc14c2cb -r 509e51b7509a src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/IsaMakefile	Wed Dec 15 11:26:28 2010 +0100
@@ -681,11 +681,11 @@
 
 HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz
 
-$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML		\
-  Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy		\
-  Metis_Examples/BT.thy Metis_Examples/Message.thy			\
-  Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy		\
-  Metis_Examples/set.thy
+$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \
+  Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \
+  Metis_Examples/BT.thy Metis_Examples/HO_Reas.thy \
+  Metis_Examples/Message.thy Metis_Examples/Tarski.thy \
+  Metis_Examples/TransClosure.thy Metis_Examples/set.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples