changeset 20253 | 636ac45d100f |
parent 20235 | 3cbf73ed92f8 |
child 20576 | 8b1591393b8d |
--- a/src/Pure/Thy/html.ML Sat Jul 29 00:51:34 2006 +0200 +++ b/src/Pure/Thy/html.ML Sat Jul 29 00:51:36 2006 +0200 @@ -413,7 +413,7 @@ val string_of_thm = Output.output o Pretty.setmp_margin 80 Pretty.string_of o - setmp show_question_marks false (ProofContext.legacy_pretty_thm false); + setmp show_question_marks false (ProofContext.pretty_thm_legacy false); fun thm th = preform (prefix_lines " " (html_mode string_of_thm th));