src/Pure/Isar/element.ML
changeset 21646 c07b5b0e8492
parent 21605 4e7307e229b3
child 21965 7120ef5bc378
     1.1 --- a/src/Pure/Isar/element.ML	Tue Dec 05 00:29:19 2006 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Tue Dec 05 00:30:38 2006 +0100
     1.3 @@ -226,7 +226,7 @@
     1.4  
     1.5  fun thm_name kind th prts =
     1.6    let val head =
     1.7 -    (case #1 (Thm.get_name_tags th) of
     1.8 +    (case PureThy.get_name_hint th of
     1.9        "" => Pretty.command kind
    1.10      | a => Pretty.block [Pretty.command kind, Pretty.brk 1, Pretty.str (Sign.base_name a ^ ":")])
    1.11    in Pretty.block (Pretty.fbreaks (head :: prts)) end;