src/HOL/Tools/function_package/fundef_common.ML

 Common definitions and other infrastructure.
 *)
 
 structure FundefCommon =
 struct
+
+local open FundefLib in
 
 (* Profiling *)
 val profile = ref false;
 
 fun PROFILE msg = if !profile then timeap_msg msg else I

 
 val default_config = FundefConfig { sequential=false, default="%x. arbitrary", 
                                     target=NONE, domintros=false, tailrec=false }
 
 
-
+end
 end
 
 (* Common Abbreviations *)
 
 structure FundefAbbrev =