--- a/src/Doc/Isar_Ref/HOL_Specific.thy Wed Dec 19 21:38:57 2018 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Dec 20 12:40:24 2018 +0000
@@ -2354,7 +2354,7 @@
( '(' target ')' '-' ? + @'and' )
;
printing_module: symbol_module ( '\<rightharpoonup>' | '=>' ) \<newline>
- ( '(' target ')' ( @{syntax string} ( @'attach' ( const + ) ) ? ) ? + @'and' )
+ ( '(' target ')' ( @{syntax string} ( @'for' ( const + ) ) ? ) ? + @'and' )
;
@@{command (HOL) code_printing} ( ( printing_const | printing_typeconstructor
| printing_class | printing_class_relation | printing_class_instance
--- a/src/Pure/Pure.thy Wed Dec 19 21:38:57 2018 +0100
+++ b/src/Pure/Pure.thy Thu Dec 20 12:40:24 2018 +0000
@@ -7,7 +7,7 @@
theory Pure
keywords
"!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
- "\<subseteq>" "]" "attach" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
+ "\<subseteq>" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
"overloaded" "pervasive" "premises" "structure" "unchecked"
and "private" "qualified" :: before_command
and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites"
--- a/src/Tools/Code/code_target.ML Wed Dec 19 21:38:57 2018 +0100
+++ b/src/Tools/Code/code_target.ML Thu Dec 20 12:40:24 2018 +0000
@@ -671,7 +671,7 @@
Outer_Syntax.command @{command_keyword code_printing} "declare dedicated printing for code symbols"
(parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax)
Parse.string (Parse.minus >> K ()) (Parse.minus >> K ())
- (Parse.text -- Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [])
+ (Parse.text -- Scan.optional (@{keyword for} |-- Scan.repeat1 Parse.term) [])
>> (Toplevel.theory o fold set_printings_cmd));
val _ =