--- a/doc-src/IsarRef/Thy/Introduction.thy Wed Jun 25 17:38:32 2008 +0200
+++ b/doc-src/IsarRef/Thy/Introduction.thy Wed Jun 25 17:38:34 2008 +0200
@@ -90,7 +90,7 @@
end;
\end{ttbox}
- Any Isabelle/Isar command may be retracted by @{command "undo"}.
+ Any Isabelle/Isar command may be retracted by @{command undo}.
See the Isabelle/Isar Quick Reference (\appref{ap:refcard}) for a
comprehensive overview of available commands and other language
elements.
@@ -219,10 +219,10 @@
The Isar proof language is embedded into the new theory format as a
proper sub-language. Proof mode is entered by stating some
- @{command "theorem"} or @{command "lemma"} at the theory level, and
- left again with the final conclusion (e.g.\ via @{command "qed"}).
+ @{command theorem} or @{command lemma} at the theory level, and
+ left again with the final conclusion (e.g.\ via @{command qed}).
A few theory specification mechanisms also require some proof, such
- as HOL's @{command "typedef"} which demands non-emptiness of the
+ as HOL's @{command typedef} which demands non-emptiness of the
representing sets.
*}
--- a/src/ZF/Tools/inductive_package.ML Wed Jun 25 17:38:32 2008 +0200
+++ b/src/ZF/Tools/inductive_package.ML Wed Jun 25 17:38:34 2008 +0200
@@ -582,7 +582,7 @@
local structure P = OuterParse and K = OuterKeyword in
-val _ = OuterSyntax.keywords
+val _ = List.app OuterKeyword.keyword
["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =