pretty_thm: quote terms (separately);
authorwenzelm
Fri Feb 12 13:55:54 1999 +0100 (1999-02-12)
changeset 6279eb4dc43023af
parent 6278 37b76155a49e
child 6280 218733fb6987
pretty_thm: quote terms (separately);
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Thu Feb 11 21:25:21 1999 +0100
     1.2 +++ b/src/Pure/display.ML	Fri Feb 12 13:55:54 1999 +0100
     1.3 @@ -52,22 +52,23 @@
     1.4      val xshyps = Thm.extra_shyps th;
     1.5      val (_, tags) = Thm.get_name_tags th;
     1.6  
     1.7 +    val prt_term = Pretty.quote o Sign.pretty_term sign;
     1.8 +
     1.9      val hlen = length xshyps + length hyps;
    1.10      val hsymbs =
    1.11        if hlen = 0 then []
    1.12        else if ! show_hyps then
    1.13          [Pretty.brk 2, Pretty.list "[" "]"
    1.14 -          (map (Sign.pretty_term sign) hyps @
    1.15 -           map (Sign.pretty_sort sign) xshyps)]
    1.16 +          (map prt_term hyps @ map (Sign.pretty_sort sign) xshyps)]
    1.17        else
    1.18          [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ "]")];
    1.19      val tsymbs =
    1.20        if null tags orelse not (! show_tags) then []
    1.21        else [Pretty.brk 1, pretty_tags tags];
    1.22 -  in Pretty.block (Sign.pretty_term sign prop :: (hsymbs @ tsymbs)) end;
    1.23 +  in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    1.24  
    1.25  val string_of_thm = Pretty.string_of o pretty_thm;
    1.26 -val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm;
    1.27 +val pprint_thm = Pretty.pprint o pretty_thm;
    1.28  
    1.29  fun pretty_thms [th] = pretty_thm th
    1.30    | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));