src/Pure/axclass.ML
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 ::