--- a/src/Pure/Pure.thy Sat Nov 14 08:45:51 2015 +0100
+++ b/src/Pure/Pure.thy Sat Nov 14 08:45:52 2015 +0100
@@ -9,7 +9,7 @@
"!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>"
"\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
"\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
- "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
+ "defines" "defining" "fixes" "for" "identifier" "if" "in" "includes" "infix"
"infixl" "infixr" "is" "notes" "obtains" "open" "output"
"overloaded" "pervasive" "premises" "private" "qualified" "rewrites"
"shows" "structure" "unchecked" "where" "when" "|"
@@ -35,7 +35,7 @@
and "include" "including" :: prf_decl
and "print_bundles" :: diag
and "context" "locale" "experiment" :: thy_decl_block
- and "sublocale" "interpretation" :: thy_goal
+ and "permanent_interpretation" "interpretation" "sublocale" :: thy_goal
and "interpret" :: prf_goal % "proof"
and "class" :: thy_decl_block
and "subclass" :: thy_goal