ProofContext.legacy_pretty_thm;
authorwenzelm
Thu Jul 27 13:43:13 2006 +0200 (2006-07-27)
changeset 202353cbf73ed92f8
parent 20234 7e0693474bcd
child 20236 54e15870444b
ProofContext.legacy_pretty_thm;
src/Pure/Isar/proof_display.ML
src/Pure/Thy/html.ML
     1.1 --- a/src/Pure/Isar/proof_display.ML	Thu Jul 27 13:43:12 2006 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Thu Jul 27 13:43:13 2006 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  structure ProofDisplay: PROOF_DISPLAY =
     1.5  struct
     1.6  
     1.7 -(* ML toplevel pretty printing *)
     1.8 +(* toplevel pretty printing *)
     1.9  
    1.10  val debug = ref false;
    1.11  
    1.12 @@ -47,7 +47,7 @@
    1.13  val pprint_term = pprint ProofContext.pretty_term;
    1.14  fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    1.15  fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    1.16 -fun pprint_thm th = pprint ProofContext.pretty_thm (Thm.theory_of_thm th) th;
    1.17 +val pprint_thm = Pretty.pprint o ProofContext.legacy_pretty_thm true;
    1.18  
    1.19  
    1.20  (* theorems and theory *)
     2.1 --- a/src/Pure/Thy/html.ML	Thu Jul 27 13:43:12 2006 +0200
     2.2 +++ b/src/Pure/Thy/html.ML	Thu Jul 27 13:43:13 2006 +0200
     2.3 @@ -411,15 +411,9 @@
     2.4  
     2.5  local
     2.6  
     2.7 -fun smart_pretty_thm th =
     2.8 -  let val thy = Thm.theory_of_thm th in
     2.9 -    if eq_thy (thy, ProtoPure.thy) then Display.pretty_thm_no_quote th
    2.10 -    else ProofContext.pretty_thm (ProofContext.init thy) th
    2.11 -  end;
    2.12 -
    2.13  val string_of_thm =
    2.14    Output.output o Pretty.setmp_margin 80 Pretty.string_of o
    2.15 -    setmp show_question_marks false smart_pretty_thm;
    2.16 +    setmp show_question_marks false (ProofContext.legacy_pretty_thm false);
    2.17  
    2.18  fun thm th = preform (prefix_lines "  " (html_mode string_of_thm th));
    2.19