rename legacy_pretty_thm to pretty_thm_legacy;
authorwenzelm
Sat Jul 29 00:51:36 2006 +0200 (2006-07-29)
changeset 20253636ac45d100f
parent 20252 bad805d0456b
child 20254 58b71535ed00
rename legacy_pretty_thm to pretty_thm_legacy;
src/Pure/Isar/proof_context.ML
src/Pure/Isar/proof_display.ML
src/Pure/Thy/html.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sat Jul 29 00:51:34 2006 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Jul 29 00:51:36 2006 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    val pretty_classrel: context -> class list -> Pretty.T
     1.5    val pretty_arity: context -> arity -> Pretty.T
     1.6    val pp: context -> Pretty.pp
     1.7 -  val legacy_pretty_thm: bool -> thm -> Pretty.T
     1.8 +  val pretty_thm_legacy: bool -> thm -> Pretty.T
     1.9    val pretty_thm: context -> thm -> Pretty.T
    1.10    val pretty_thms: context -> thm list -> Pretty.T
    1.11    val pretty_fact: context -> string * thm list -> Pretty.T
    1.12 @@ -281,7 +281,7 @@
    1.13  fun pp ctxt = Pretty.pp (pretty_term ctxt, pretty_typ ctxt, pretty_sort ctxt,
    1.14    pretty_classrel ctxt, pretty_arity ctxt);
    1.15  
    1.16 -fun legacy_pretty_thm quote th =
    1.17 +fun pretty_thm_legacy quote th =
    1.18    let
    1.19      val thy = Thm.theory_of_thm th;
    1.20      val pp =
     2.1 --- a/src/Pure/Isar/proof_display.ML	Sat Jul 29 00:51:34 2006 +0200
     2.2 +++ b/src/Pure/Isar/proof_display.ML	Sat Jul 29 00:51:36 2006 +0200
     2.3 @@ -47,7 +47,7 @@
     2.4  val pprint_term = pprint ProofContext.pretty_term;
     2.5  fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
     2.6  fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
     2.7 -val pprint_thm = Pretty.pprint o ProofContext.legacy_pretty_thm true;
     2.8 +val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy true;
     2.9  
    2.10  
    2.11  (* theorems and theory *)
     3.1 --- a/src/Pure/Thy/html.ML	Sat Jul 29 00:51:34 2006 +0200
     3.2 +++ b/src/Pure/Thy/html.ML	Sat Jul 29 00:51:36 2006 +0200
     3.3 @@ -413,7 +413,7 @@
     3.4  
     3.5  val string_of_thm =
     3.6    Output.output o Pretty.setmp_margin 80 Pretty.string_of o
     3.7 -    setmp show_question_marks false (ProofContext.legacy_pretty_thm false);
     3.8 +    setmp show_question_marks false (ProofContext.pretty_thm_legacy false);
     3.9  
    3.10  fun thm th = preform (prefix_lines "  " (html_mode string_of_thm th));
    3.11