| changeset 21051 | c49467a9c1e1 |
| parent 20654 | d80502f0d701 |
| child 21237 | b803f9870e97 |
--- 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 __ *)