--- a/src/Doc/Isar_Ref/HOL_Specific.thy Sat Jun 11 13:57:59 2016 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Sat Jun 11 16:41:11 2016 +0200
@@ -108,7 +108,7 @@
@{rail \<open>
(@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
@@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
- @{syntax "fixes"} @{syntax "for_fixes"} \<newline>
+ @{syntax vars} @{syntax for_fixes} \<newline>
(@'where' @{syntax multi_specs})? (@'monos' @{syntax thms})?
;
@@{command print_inductives} ('!'?)