equal
deleted
inserted
replaced
58 fun pretty_const ctxt (nm, ty) = |
58 fun pretty_const ctxt (nm, ty) = |
59 let |
59 let |
60 val ty' = Logic.unvarifyT_global ty; |
60 val ty' = Logic.unvarifyT_global ty; |
61 in |
61 in |
62 Pretty.block |
62 Pretty.block |
63 [Pretty.quote (Pretty.str nm), Pretty.fbrk, |
63 [Pretty.str nm, Pretty.str " ::", Pretty.brk 1, |
64 Pretty.str "::", Pretty.brk 1, |
|
65 Pretty.quote (Syntax.pretty_typ ctxt ty')] |
64 Pretty.quote (Syntax.pretty_typ ctxt ty')] |
66 end; |
65 end; |
67 |
66 |
68 |
67 |
69 (* find_consts *) |
68 (* find_consts *) |