src/Pure/Thy/thy_output.ML
changeset 35399 3881972fcfca
parent 33957 e9afca2118d4
child 36163 823c9400eb62
     1.1 --- a/src/Pure/Thy/thy_output.ML	Sat Feb 27 13:55:03 2010 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Feb 27 20:51:51 2010 +0100
     1.3 @@ -528,7 +528,7 @@
     1.4  val _ = basic_entity "term" (Term_Style.parse -- Args.term) pretty_term_style;
     1.5  val _ = basic_entity "term_type" (Term_Style.parse -- Args.term) pretty_term_typ;
     1.6  val _ = basic_entity "typeof" (Term_Style.parse -- Args.term) pretty_term_typeof;
     1.7 -val _ = basic_entity "const" Args.const_proper pretty_const;
     1.8 +val _ = basic_entity "const" (Args.const_proper false) pretty_const;
     1.9  val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
    1.10  val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
    1.11  val _ = basic_entity "text" (Scan.lift Args.name) (K pretty_text);