changeset 2238 | c72a23bbe762 |
parent 1475 | 7f5a4cd08209 |
child 2851 | b6a5780e36b9 |
--- a/src/HOL/typedef.ML Wed Nov 27 10:36:38 1996 +0100 +++ b/src/HOL/typedef.ML Wed Nov 27 10:40:45 1996 +0100 @@ -80,7 +80,7 @@ (* errors *) - val show_names = commas_quote o map fst; + fun show_names pairs = commas_quote (map fst pairs); val illegal_vars = if null (term_vars set) andalso null (term_tvars set) then []