--- 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 *)