# HG changeset patch
# User wenzelm
# Date 1116346241 -7200
# Node ID 181bbcee76f5137d612e95cd487ff503648427ad
# Parent  35ec4802c66c0481320b330953cdf3926c11cb98
renamed show_var_qmarks to show_question_marks;
renamed TermStyle.lookup_style to TermStyle.the_style;

diff -r 35ec4802c66c -r 181bbcee76f5 src/Pure/Isar/isar_output.ML
--- 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;
-