src/Pure/axclass.ML
changeset 16364 dc9f7066d80a
parent 16333 490d77820631
child 16458 4c6fd0c01d28
     1.1 --- a/src/Pure/axclass.ML	Sat Jun 11 22:15:47 2005 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sat Jun 11 22:15:48 2005 +0200
     1.3 @@ -131,12 +131,9 @@
     1.4  
     1.5    fun print sg tab =
     1.6      let
     1.7 -      val ext_class = Sign.extern sg Sign.classK;
     1.8 -      val ext_thm = PureThy.extern_thm_sg sg;
     1.9 -
    1.10        fun pretty_class c cs = Pretty.block
    1.11 -        (Pretty.str (ext_class c) :: Pretty.str " <" :: Pretty.brk 1 ::
    1.12 -          Pretty.breaks (map (Pretty.str o ext_class) cs));
    1.13 +        (Pretty.str (Sign.extern_class sg c) :: Pretty.str " <" :: Pretty.brk 1 ::
    1.14 +          Pretty.breaks (map (Pretty.str o Sign.extern_class sg) cs));
    1.15  
    1.16        fun pretty_thms name thms = Pretty.big_list (name ^ ":")
    1.17          (map (Display.pretty_thm_sg sg) thms);
    1.18 @@ -282,7 +279,7 @@
    1.19  fun prep_arity prep_tycon prep_sort prep sg (t, Ss, x) =
    1.20    test_arity sg (prep_tycon sg t, map (prep_sort sg) Ss, prep sg x);
    1.21  
    1.22 -val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
    1.23 +val read_arity = prep_arity Sign.intern_type Sign.read_sort Sign.read_sort;
    1.24  val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
    1.25  
    1.26