more formal markup;
authorwenzelm
Wed Oct 17 10:26:27 2012 +0200 (2012-10-17)
changeset 498860dc57c05bf4e
parent 49885 b0d6d2e7a522
child 49887 1a173b2503c0
more formal markup;
src/Pure/Tools/find_consts.ML
     1.1 --- a/src/Pure/Tools/find_consts.ML	Wed Oct 17 00:16:31 2012 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Wed Oct 17 10:26:27 2012 +0200
     1.3 @@ -55,12 +55,14 @@
     1.4      | Name name => Pretty.str (prfx "name: " ^ quote name))
     1.5    end;
     1.6  
     1.7 -fun pretty_const ctxt (nm, ty) =
     1.8 +fun pretty_const ctxt (c, ty) =
     1.9    let
    1.10      val ty' = Logic.unvarifyT_global ty;
    1.11 +    val consts_space = Consts.space_of (Sign.consts_of (Proof_Context.theory_of ctxt));
    1.12 +    val markup = Name_Space.markup consts_space c;
    1.13    in
    1.14      Pretty.block
    1.15 -     [Pretty.str nm, Pretty.str " ::", Pretty.brk 1,
    1.16 +     [Pretty.mark markup (Pretty.str c), Pretty.str " ::", Pretty.brk 1,
    1.17        Pretty.quote (Syntax.pretty_typ ctxt ty')]
    1.18    end;
    1.19