changeset 19770 | be5c23ebe1eb |
parent 19564 | d3e2f532459a |
child 19841 | f2fa72c13186 |
--- a/src/HOL/Tools/function_package/fundef_lib.ML Mon Jun 05 14:22:58 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_lib.ML Mon Jun 05 14:26:07 2006 +0200 @@ -62,3 +62,6 @@ fun upairs [] = [] | upairs (x::xs) = map (pair x) (x::xs) @ upairs xs + +fun the_single [x] = x + | the_single _ = sys_error "the_single" \ No newline at end of file