pretty_thm_no_quote;
authorwenzelm
Tue Mar 09 12:07:52 1999 +0100 (1999-03-09)
changeset 631447c801a77f32
parent 6313 6e4c7209ff39
child 6315 ed71bedf6976
pretty_thm_no_quote;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Tue Mar 09 12:07:32 1999 +0100
     1.2 +++ b/src/Pure/display.ML	Tue Mar 09 12:07:52 1999 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4  sig
     1.5    val show_hyps		: bool ref
     1.6    val show_tags		: bool ref
     1.7 +  val pretty_thm_no_quote: thm -> Pretty.T
     1.8    val pretty_thm	: thm -> Pretty.T
     1.9    val pretty_thms	: thm list -> Pretty.T
    1.10    val string_of_thm	: thm -> string
    1.11 @@ -46,13 +47,13 @@
    1.12  fun pretty_tag (name, args) = Pretty.strs (name :: args);
    1.13  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    1.14  
    1.15 -fun pretty_thm th =
    1.16 +fun pretty_thm_aux quote th =
    1.17    let
    1.18      val {sign, hyps, prop, ...} = rep_thm th;
    1.19      val xshyps = Thm.extra_shyps th;
    1.20      val (_, tags) = Thm.get_name_tags th;
    1.21  
    1.22 -    val prt_term = Pretty.quote o Sign.pretty_term sign;
    1.23 +    val prt_term = (if quote then Pretty.quote else I) o Sign.pretty_term sign;
    1.24  
    1.25      val hlen = length xshyps + length hyps;
    1.26      val hsymbs =
    1.27 @@ -67,6 +68,9 @@
    1.28        else [Pretty.brk 1, pretty_tags tags];
    1.29    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    1.30  
    1.31 +val pretty_thm_no_quote = pretty_thm_aux false;
    1.32 +val pretty_thm = pretty_thm_aux true;
    1.33 +
    1.34  val string_of_thm = Pretty.string_of o pretty_thm;
    1.35  val pprint_thm = Pretty.pprint o pretty_thm;
    1.36