changeset 14824 | 336ade035a34 |
parent 14643 | 130076a81b84 |
child 14854 | 61bdf2ae4dc5 |
--- a/src/Pure/drule.ML Sat May 29 15:00:25 2004 +0200 +++ b/src/Pure/drule.ML Sat May 29 15:00:52 2004 +0200 @@ -297,7 +297,7 @@ (*Strip extraneous shyps as far as possible*) fun strip_shyps_warning thm = let - val str_of_sort = Sign.str_of_sort (Thm.sign_of_thm thm); + val str_of_sort = Pretty.str_of o Sign.pretty_sort (Thm.sign_of_thm thm); val thm' = Thm.strip_shyps thm; val xshyps = Thm.extra_shyps thm'; in