src/Pure/Tools/find_consts.ML
changeset 49886 0dc57c05bf4e
parent 48646 91281e9472d8
child 50214 67fb9a168d10
     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