1.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Jan 04 00:52:48 2006 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Jan 04 00:52:49 2006 +0100
     1.3 @@ -51,6 +51,7 @@
     1.4        token_translation: (string * string * (string -> string * real)) list}
     1.5    val mfix_args: string -> int
     1.6    val escape_mfix: string -> string
     1.7 +  val unlocalize_mfix: string -> string
     1.8    val syn_ext': bool -> (string -> bool) -> mfix list ->
     1.9      string list -> (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list *
    1.10      (string * ((theory -> term list -> term) * stamp)) list *
    1.11 @@ -232,6 +233,14 @@
    1.12    val escape_mfix = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
    1.13  end;
    1.14  
    1.15 +val unlocalize_mfix =
    1.16 +  let
    1.17 +    fun unloc ("'" :: "\\<^loc>" :: ss) = unloc ss
    1.18 +      | unloc ("\\<^loc>" :: ss) = unloc ss
    1.19 +      | unloc (s :: ss) = s :: unloc ss
    1.20 +      | unloc [] = [];
    1.21 +  in Symbol.explode #> unloc #> implode end;  
    1.22 +
    1.23  
    1.24  (* mfix_to_xprod *)
    1.25