| changeset 56220 | 4c43a2881b25 |
| parent 56161 | 300f613060b0 |
| child 56243 | 2e10a36b8d46 |
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Mar 19 21:59:31 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Mar 19 22:10:33 2014 +0100 @@ -444,7 +444,7 @@ fun pretty_for_type ctxt = Syntax.pretty_typ ctxt o unarize_unbox_etc_type val prefix_name = Long_Name.qualify o Long_Name.base_name -fun shortest_name s = List.last (space_explode "." s) handle List.Empty => "" +val shortest_name = Long_Name.base_name val prefix_abs_vars = Term.map_abs_vars o prefix_name fun short_name s =