src/HOL/FunDef.thy

 
 theory FunDef
 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")
   ("Tools/function_package/mutual.ML")
   ("Tools/function_package/pattern_split.ML")

     by (rule THE_default_none)
 qed
 
 
 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"
 use "Tools/function_package/mutual.ML"
 use "Tools/function_package/pattern_split.ML"