changeset 16122 | 864fda4a4056 |
parent 15973 | 5fd94d84470f |
child 16180 | a51be5cbd81d |
--- a/src/Pure/axclass.ML Tue May 31 11:53:12 2005 +0200 +++ b/src/Pure/axclass.ML Tue May 31 11:53:13 2005 +0200 @@ -131,8 +131,8 @@ fun print sg tab = let - val ext_class = Sign.cond_extern sg Sign.classK; - val ext_thm = PureThy.cond_extern_thm_sg sg; + val ext_class = Sign.extern sg Sign.classK; + val ext_thm = PureThy.extern_thm_sg sg; fun pretty_class c cs = Pretty.block (Pretty.str (ext_class c) :: Pretty.str " <" :: Pretty.brk 1 ::