+
+ let unquote = ref false
+
+(* This turns an Automath identifier into an XML nmtoken *)
+ let quote id =
+ let l = String.length id in
+ let rec aux i =
+ if i < l then begin
+ if id.[i] = '\'' || id.[i] = '`' then id.[i] <- '_';
+ aux (succ i)
+ end else
+ id
+ in
+ aux 0