renamed show_var_qmarks to show_question_marks;
authorwenzelm
Tue, 17 May 2005 18:10:41 +0200
changeset 15988 181bbcee76f5
parent 15987 35ec4802c66c
child 15989 80dd2f5780df
renamed show_var_qmarks to show_question_marks; renamed TermStyle.lookup_style to TermStyle.the_style;
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;
-