removed obsolete unlocalize_mfix;
authorwenzelm
Wed, 17 Oct 2007 23:16:38 +0200
changeset 25075 8717d93b0fe2
parent 25074 78fdb4c44939
child 25076 a50b36401c61
removed obsolete unlocalize_mfix;
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 *)