--- a/src/Pure/Thy/thy_output.ML Thu Mar 06 12:58:51 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Thu Mar 06 13:44:01 2014 +0100
@@ -573,7 +573,7 @@
basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
- basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
+ basic_entity (Binding.name "const") (Args.const {proper = true, strict = false}) pretty_const #>
basic_entity (Binding.name "abbrev") (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>