src/HOLCF/IOA/meta_theory/ioa_syn.ML

   (name -- ("=" $$--
         ("restrict" $$-- name --
                 ("to" $$-- (enum1 "," string)))) >> mk_restriction_decl)
 ||
   (name -- ("=" $$--
-	("rename" $$-- name -- ("with" $$-- string))) >> mk_rename_decl)
+	("rename" $$-- name -- ("using" $$-- string))) >> mk_rename_decl)
 ;
 
 in
 (******************************************************************)
 (* im folgenden werden in der ersten Liste alle beim Einlesen von *)

 (* mitsamt dessen Einlesepattern ioa_decl                         *)
 (******************************************************************)
 val _ = ThySyn.add_syntax
  ["signature","actions","inputs", "outputs", "internals", "states", "initially",
   "transitions", "pre", "post", "transrel",":=",
-"compose","hide","in","restrict","to","rename","with"]
+"compose","hide","in","restrict","to","rename","using"]
  [axm_section "automaton" "" ioa_decl];
 
 end;