# HG changeset patch
# User wenzelm
# Date 1136332369 -3600
# Node ID 20dd2f7dca4b9595c6c26cca51eb7ca143819a12
# Parent  818a24371de9e5f625232756aae74263e6bf9bec
added unlocalize_mfix;

diff -r 818a24371de9 -r 20dd2f7dca4b src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Wed Jan 04 00:52:48 2006 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Wed Jan 04 00:52:49 2006 +0100
@@ -51,6 +51,7 @@
       token_translation: (string * string * (string -> string * real)) list}
   val mfix_args: string -> int
   val escape_mfix: string -> string
+  val unlocalize_mfix: string -> string
   val syn_ext': bool -> (string -> bool) -> mfix list ->
     string list -> (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((theory -> term list -> term) * stamp)) list *
@@ -232,6 +233,14 @@
   val escape_mfix = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
 end;
 
+val unlocalize_mfix =
+  let
+    fun unloc ("'" :: "\\<^loc>" :: ss) = unloc ss
+      | unloc ("\\<^loc>" :: ss) = unloc ss
+      | unloc (s :: ss) = s :: unloc ss
+      | unloc [] = [];
+  in Symbol.explode #> unloc #> implode end;  
+
 
 (* mfix_to_xprod *)