# HG changeset patch
# User wenzelm
# Date 1183494428 -7200
# Node ID 151d60fbfffe26fae63bf4d3002ca9f28908d6db
# Parent  af8ae54238f5488be976e53efc3166cf7e72f627
proper use of function_package ML files;

diff -r af8ae54238f5 -r 151d60fbfffe src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jul 03 22:27:05 2007 +0200
+++ b/src/HOL/List.thy	Tue Jul 03 22:27:08 2007 +0200
@@ -8,6 +8,8 @@
 theory List
 imports PreList
 uses "Tools/string_syntax.ML"
+  ("Tools/function_package/lexicographic_order.ML")
+  ("Tools/function_package/fundef_datatype.ML")
 begin
 
 datatype 'a list =