# HG changeset patch
# User wenzelm
# Date 1180905403 -7200
# Node ID 20b5558a54198480203c9944e645f6002c6f8ae4
# Parent  dc23c062b58c297613bddb2aa704f7d861414b7e
local open FundefLib;

diff -r dc23c062b58c -r 20b5558a5419 src/HOL/Tools/function_package/fundef_common.ML
--- 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 *)