changeset 59433 | 9da5b2c61049 |
parent 59058 | a78612c67ec0 |
child 59582 | 0fbed69ff081 |
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Jan 24 21:37:31 2015 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Jan 24 22:00:24 2015 +0100 @@ -320,7 +320,7 @@ fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep fun quot_normal_name_for_type ctxt T = - quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T) + quot_normal_prefix ^ YXML.content_of (Syntax.string_of_typ ctxt T) val strip_first_name_sep = Substring.full #> Substring.position name_sep ##> Substring.triml 1