--- a/src/Pure/Isar/element.ML Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/Isar/element.ML Thu Aug 14 16:52:46 2008 +0200
@@ -228,9 +228,9 @@
fun thm_name kind th prts =
let val head =
- if PureThy.has_name_hint th then
+ if Thm.has_name_hint th then
Pretty.block [Pretty.command kind,
- Pretty.brk 1, Pretty.str (Sign.base_name (PureThy.get_name_hint th) ^ ":")]
+ Pretty.brk 1, Pretty.str (Sign.base_name (Thm.get_name_hint th) ^ ":")]
else Pretty.command kind
in Pretty.block (Pretty.fbreaks (head :: prts)) end;