src/HOL/Tools/record_package.ML
changeset 16364 dc9f7066d80a
parent 16330 934219e919e4
child 16379 d29d27e0f59f
     1.1 --- a/src/HOL/Tools/record_package.ML	Sat Jun 11 22:15:47 2005 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Sat Jun 11 22:15:48 2005 +0200
     1.3 @@ -287,7 +287,7 @@
     1.4              [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
     1.5  
     1.6        fun pretty_field (c, T) = Pretty.block
     1.7 -        [Pretty.str (Sign.extern sg Sign.constK c), Pretty.str " ::",
     1.8 +        [Pretty.str (Sign.extern_const sg c), Pretty.str " ::",
     1.9            Pretty.brk 1, Pretty.quote (prt_typ T)];
    1.10  
    1.11        fun pretty_record (name, {args, parent, fields, ...}: record_info) =
    1.12 @@ -670,7 +670,7 @@
    1.13                       SOME flds 
    1.14                       => (let
    1.15                            val (f::fs) = but_last (map fst flds);
    1.16 -                          val flds' = Sign.extern sg Sign.constK f::map NameSpace.base fs; 
    1.17 +                          val flds' = Sign.extern_const sg f :: map NameSpace.base fs; 
    1.18                            val (args',more) = split_last args; 
    1.19                           in (flds'~~args')@field_lst more end
    1.20                           handle UnequalLengths => [("",t)])
    1.21 @@ -775,7 +775,7 @@
    1.22                             SOME (_,alphas) 
    1.23                             => (let
    1.24                                  val (f::fs) = but_last flds;
    1.25 -                                val flds' = apfst (Sign.extern sg Sign.constK) f
    1.26 +                                val flds' = apfst (Sign.extern_const sg) f
    1.27                                              ::map (apfst NameSpace.base) fs; 
    1.28                                  val (args',more) = split_last args; 
    1.29                                  val alphavars = map Type.varifyT (but_last alphas);