diff -r 98736a2fec98 -r a5026e73cfcf src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Sat Jun 02 15:26:32 2007 +0200
+++ b/src/HOL/FunDef.thy	Sat Jun 02 15:28:38 2007 +0200
@@ -9,8 +9,8 @@
 imports Datatype Accessible_Part
 uses
   ("Tools/function_package/sum_tools.ML")
+  ("Tools/function_package/fundef_lib.ML")
   ("Tools/function_package/fundef_common.ML")
-  ("Tools/function_package/fundef_lib.ML")
   ("Tools/function_package/inductive_wrap.ML")
   ("Tools/function_package/context_tree.ML")
   ("Tools/function_package/fundef_core.ML")
@@ -88,8 +88,8 @@
 
 
 use "Tools/function_package/sum_tools.ML"
+use "Tools/function_package/fundef_lib.ML"
 use "Tools/function_package/fundef_common.ML"
-use "Tools/function_package/fundef_lib.ML"
 use "Tools/function_package/inductive_wrap.ML"
 use "Tools/function_package/context_tree.ML"
 use "Tools/function_package/fundef_core.ML"