src/HOL/FunDef.thy
changeset 23203 a5026e73cfcf
parent 22919 3de2d0b5b89a
child 23494 f985f9239e0d
--- 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"