diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOLCF/IOA/meta_theory/ioa_package.ML
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -481,10 +481,15 @@
   add_rename aut source_aut rename_f;
 
 
-(* parsers *)
+(* outer syntax *)
 
 local structure P = OuterParse and K = OuterKeyword in
 
+val _ = OuterSyntax.keywords ["signature", "actions", "inputs",
+  "outputs", "internals", "states", "initially", "transitions", "pre",
+  "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
+  "rename"];
+
 val actionlist = P.list1 P.term;
 val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
 val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
@@ -520,21 +525,10 @@
   (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
     >> mk_rename_decl;
 
-val automatonP =
+val _ =
   OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
     (ioa_decl >> Toplevel.theory);
 
 end;
 
-
-(* setup outer syntax *)
-
-val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs",
-  "outputs", "internals", "states", "initially", "transitions", "pre",
-  "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
-  "rename"];
-
-val _ = OuterSyntax.add_parsers [automatonP];
-
-
 end;