src/Pure/Syntax/syn_ext.ML

       print_translation: (string * (bool -> typ -> term list -> term)) list,
       print_rules: (Ast.ast * Ast.ast) list,
       print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
       token_translation: (string * string * (string -> string * real)) list}
   val mfix_args: string -> int
+  val escape_mfix: string -> string
   val mk_syn_ext: bool -> string list -> mfix list ->
     string list -> (string * (Ast.ast list -> Ast.ast)) list *
     (string * (term list -> term)) list *
     (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
     -> (string * string * (string -> string * real)) list

     if length (filter is_index xsymbs) <= 1 then xsymbs
     else error "Duplicate index arguments (\\<index>)";
 in
   val read_mixfix = unique_index o read_symbs o Symbol.explode;
   val mfix_args = length o filter is_argument o read_mixfix;
+  val escape_mfix = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
 end;
 
 
 (* mfix_to_xprod *)