diff -r d0447a511edb -r c49467a9c1e1 src/HOL/Tools/function_package/pattern_split.ML
--- a/src/HOL/Tools/function_package/pattern_split.ML	Wed Oct 18 10:15:39 2006 +0200
+++ b/src/HOL/Tools/function_package/pattern_split.ML	Wed Oct 18 16:13:03 2006 +0200
@@ -21,6 +21,7 @@
 structure FundefSplit : FUNDEF_SPLIT =
 struct
 
+open FundefLib
 
 (* We use proof context for the variable management *)
 (* FIXME: no __ *)