removed obsolete pretty_thm_no_quote;
authorwenzelm
Thu Jul 27 13:43:04 2006 +0200 (2006-07-27)
changeset 202266ea469c03314
parent 20225 4b8e42490e58
child 20227 435601e8e53d
removed obsolete pretty_thm_no_quote;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Thu Jul 27 13:43:03 2006 +0200
     1.2 +++ b/src/Pure/display.ML	Thu Jul 27 13:43:04 2006 +0200
     1.3 @@ -33,7 +33,6 @@
     1.4    val raw_string_of_term: term -> string
     1.5    val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
     1.6    val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
     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 pretty_thm_sg: theory -> thm -> Pretty.T
    1.11 @@ -100,12 +99,8 @@
    1.12        else [Pretty.brk 1, pretty_tags tags];
    1.13    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    1.14  
    1.15 -fun gen_pretty_thm quote th =
    1.16 -  pretty_thm_aux (Sign.pp (Thm.theory_of_thm th)) quote false [] th;
    1.17 -
    1.18 -val pretty_thm = gen_pretty_thm true;
    1.19 -val pretty_thm_no_quote = gen_pretty_thm false;
    1.20 -
    1.21 +fun pretty_thm th =
    1.22 +  pretty_thm_aux (Sign.pp (Thm.theory_of_thm th)) true false [] th;
    1.23  
    1.24  val string_of_thm = Pretty.string_of o pretty_thm;
    1.25