X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fautomath%2FautLexer.mll;h=58324a0216c71e2c693a3d0ca5169a2a7a193e93;hb=25893b01cb815cbd9a3b9684952bfc0f42c0739d;hp=5a7155e4a56db66a0aa153c02b9b8cd121180856;hpb=bcc6a96020485731da4c02cc38043817903bd7dc;p=helm.git

diff --git a/helm/software/helena/src/automath/autLexer.mll b/helm/software/helena/src/automath/autLexer.mll
index 5a7155e4a..58324a021 100644
--- a/helm/software/helena/src/automath/autLexer.mll
+++ b/helm/software/helena/src/automath/autLexer.mll
@@ -10,6 +10,8 @@
       V_______________________________________________________________ *)
 
 { 
+   module KT = String
+
    module L  = Log
    module G  = Options
    module AP = AutParser
@@ -23,15 +25,12 @@ END
 IFDEF QUOTE THEN
 (* 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
+      let map = function
+         | '\''
+         | '`' -> '_';
+         | c   -> c
       in
-      aux 0
+      KT.map map id
 
 END
 }