# HG changeset patch
# User wenzelm
# Date 1192655798 -7200
# Node ID 8717d93b0fe2217766d0b4b83afc7ebd184bb346
# Parent  78fdb4c449398aaf92d34d4a521371dbbcaf7868
removed obsolete unlocalize_mfix;

diff -r 78fdb4c44939 -r 8717d93b0fe2 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Wed Oct 17 23:16:36 2007 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Wed Oct 17 23:16:38 2007 +0200
@@ -53,7 +53,6 @@
   val mfix_delims: string -> string 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 * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
@@ -232,14 +231,6 @@
 
 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 *)