# HG changeset patch
# User wenzelm
# Date 1012395929 -3600
# Node ID 6b3484b8d5725f68738ce2d29701baae62dd0f21
# Parent  cecaa6e64fd5c692741445c5c7413b8d02ac824f
escape_mfix;

diff -r cecaa6e64fd5 -r 6b3484b8d572 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Wed Jan 30 14:00:36 2002 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Wed Jan 30 14:05:29 2002 +0100
@@ -46,6 +46,7 @@
       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 *
@@ -216,6 +217,7 @@
 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;