--- a/src/Pure/Thy/thy_output.ML Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Wed Jan 22 16:03:11 2014 +0100
@@ -570,9 +570,9 @@
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 "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
+ 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_source) pretty_class #>
+ basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>