| changeset 33099 | b8cdd3d73022 |
| parent 33083 | 1fad3160d873 |
| child 36945 | 9bec62c10714 |
--- a/src/HOL/Tools/Function/pat_completeness.ML Fri Oct 23 15:33:19 2009 +0200 +++ b/src/HOL/Tools/Function/pat_completeness.ML Fri Oct 23 16:22:10 2009 +0200 @@ -17,8 +17,8 @@ structure Pat_Completeness : PAT_COMPLETENESS = struct -open FundefLib -open FundefCommon +open Function_Lib +open Function_Common fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)