# HG changeset patch
# User haftmann
# Date 1545309624 0
# Node ID ed6b100a9c7d2ae55da7bb8544bf63e14a1495f1
# Parent  023d92df3d845c58da3c92a6c8620fdb9e1107a9
disregard historic keyword

diff -r 023d92df3d84 -r ed6b100a9c7d src/Doc/Isar_Ref/HOL_Specific.thy
--- 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
diff -r 023d92df3d84 -r ed6b100a9c7d src/Pure/Pure.thy
--- 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"
diff -r 023d92df3d84 -r ed6b100a9c7d src/Tools/Code/code_target.ML
--- 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 _ =