--- 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"