
diff -r c20946f5b6fb -r e9c777bfd78c src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Sat Jun 11 13:57:59 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Sat Jun 11 16:41:11 2016 +0200
@@ -354,7 +354,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command axiomatization} @{syntax "fixes"}? (@'where' axiomatization)?
+    @@{command axiomatization} @{syntax vars}? (@'where' axiomatization)?
     ;
     axiomatization: (@{syntax thmdecl} @{syntax prop} + @'and')
       @{syntax spec_prems} @{syntax for_fixes}
@@ -516,7 +516,7 @@
       @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
     ;
     @{syntax_def context_elem}:
-      @'fixes' @{syntax "fixes"} |
+      @'fixes' @{syntax vars} |
       @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
       @'assumes' (@{syntax props} + @'and') |
       @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |




