| changeset 21051 | c49467a9c1e1 |
| parent 20999 | 9131d8e96dba |
| child 21211 | 5370cfbf3070 |
--- a/src/HOL/Tools/function_package/fundef_datatype.ML Wed Oct 18 10:15:39 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Wed Oct 18 16:13:03 2006 +0200 @@ -17,6 +17,8 @@ structure FundefDatatype : FUNDEF_DATATYPE = struct +open FundefLib +open FundefCommon fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T) fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)