renamed show_var_qmarks to show_question_marks;
renamed TermStyle.lookup_style to TermStyle.the_style;
--- a/src/Pure/Isar/isar_output.ML Tue May 17 18:10:40 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML Tue May 17 18:10:41 2005 +0200
@@ -297,7 +297,7 @@
[("show_types", Library.setmp Syntax.show_types o boolean),
("show_sorts", Library.setmp Syntax.show_sorts o boolean),
("show_structs", Library.setmp show_structs o boolean),
- ("show_var_qmarks", Library.setmp show_var_qmarks o boolean),
+ ("show_question_marks", Library.setmp show_question_marks o boolean),
("long_names", Library.setmp NameSpace.long_names o boolean),
("eta_contract", Library.setmp Syntax.eta_contract o boolean),
("locale", Library.setmp locale),
@@ -368,7 +368,7 @@
fun pretty_term_style ctxt (name, term) =
let
val thy = ProofContext.theory_of ctxt
- in pretty_term ctxt (TermStyle.lookup_style thy name ctxt term) end;
+ in pretty_term ctxt (TermStyle.the_style thy name ctxt term) end;
fun pretty_thm_style ctxt (name, thm) = pretty_term_style ctxt (name, Thm.prop_of thm);
@@ -408,4 +408,3 @@
("full_prf", args Attrib.local_thmss (output_with (pretty_prf true)))];
end;
-