local open FundefLib;

--- a/src/HOL/Tools/function_package/fundef_common.ML	Sun Jun 03 23:16:42 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Sun Jun 03 23:16:43 2007 +0200
@@ -9,6 +9,8 @@
 structure FundefCommon =
 struct
 
+local open FundefLib in
+
 (* Profiling *)
 val profile = ref false;
 
@@ -326,7 +328,7 @@
                                     target=NONE, domintros=false, tailrec=false }
 
 
-
+end
 end
 
 (* Common Abbreviations *)