# HG changeset patch
# User krauss
# Date 1210662847 -7200
# Node ID 1aeac4d6b3771681188da91f6266c2b55fedc42f
# Parent  c3bb1f39781125c4c3c58585d6dffdbda279f038
fixed makefile

diff -r c3bb1f397811 -r 1aeac4d6b377 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue May 13 09:10:56 2008 +0200
+++ b/src/HOL/IsaMakefile	Tue May 13 09:14:07 2008 +0200
@@ -126,6 +126,7 @@
   Tools/function_package/fundef_package.ML				\
   Tools/function_package/inductive_wrap.ML				\
   Tools/function_package/lexicographic_order.ML				\
+  Tools/function_package/measure_functions.ML	\
   Tools/function_package/mutual.ML					\
   Tools/function_package/pattern_split.ML	\
   Tools/function_package/size.ML Tools/inductive_codegen.ML	\