# HG changeset patch
# User wenzelm
# Date 1214408314 -7200
# Node ID f7ba6b2af22a5c38658a119804dc9c70e9e60b43
# Parent  71c4dd53d4cbcf1af3daa6876352875f5f464755
tuned;

diff -r 71c4dd53d4cb -r f7ba6b2af22a doc-src/IsarRef/Thy/Introduction.thy
--- 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.
 *}
 
diff -r 71c4dd53d4cb -r f7ba6b2af22a src/ZF/Tools/inductive_package.ML
--- 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) =