# HG changeset patch
# User wenzelm
# Date 1267221947 -3600
# Node ID efad0e36473825573dbde36f05a234a36cb5ddb5
# Parent  2be5440f7271eb7918faa90a2c5e3c2e98b4a496
use simplified Syntax.escape;

diff -r 2be5440f7271 -r efad0e364738 src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Feb 26 21:43:26 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Feb 26 23:05:47 2010 +0100
@@ -49,25 +49,14 @@
   if line = 0 orelse col = 0 then no_label_name
   else label_prefix ^ string_of_int line ^ "_" ^ string_of_int col
 
-local
-  val quote_mixfix =
-    Symbol.explode #> map
-      (fn "_" => "'_"
-        | "(" => "'("
-        | ")" => "')"
-        | "/" => "'/"
-        | s => s) #>
-    implode
-in
 fun mk_syntax name i =
   let
-    val syn = quote_mixfix name
+    val syn = Syntax.escape name
     val args = concat (separate ",/ " (replicate i "_"))
   in
     if i = 0 then Mixfix (syn, [], 1000)
     else Mixfix (syn ^ "()'(/" ^ args ^ "')", replicate i 0, 1000)
   end
-end
 
 
 datatype attribute_value = StringValue of string | TermValue of term
diff -r 2be5440f7271 -r efad0e364738 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Fri Feb 26 21:43:26 2010 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Fri Feb 26 23:05:47 2010 +0100
@@ -186,7 +186,7 @@
 
 fun mk_syn thy c =
   if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn
-  else Syntax.literal c
+  else Delimfix (Syntax.escape c)
 
 fun quotename c =
   if Syntax.is_identifier c andalso not (OuterKeyword.is_keyword c) then c else quote c
diff -r 2be5440f7271 -r efad0e364738 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Feb 26 21:43:26 2010 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Fri Feb 26 23:05:47 2010 +0100
@@ -21,7 +21,6 @@
 signature MIXFIX1 =
 sig
   include MIXFIX0
-  val literal: string -> mixfix
   val no_syn: 'a * 'b -> 'a * 'b * mixfix
   val pretty_mixfix: mixfix -> Pretty.T
   val mixfix_args: mixfix -> int
@@ -51,8 +50,6 @@
   Binder of string * int * int |
   Structure;
 
-val literal = Delimfix o SynExt.escape_mfix;
-
 fun no_syn (x, y) = (x, y, NoSyn);
 
 
diff -r 2be5440f7271 -r efad0e364738 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Fri Feb 26 21:43:26 2010 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Fri Feb 26 23:05:47 2010 +0100
@@ -14,6 +14,7 @@
   val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
   val mk_trfun: string * 'a -> string * ('a * stamp)
   val eq_trfun: ('a * stamp) * ('a * stamp) -> bool
+  val escape: string -> string
   val tokentrans_mode:
     string -> (string * (Proof.context -> string -> Pretty.T)) list ->
     (string * string * (Proof.context -> string -> Pretty.T)) list
@@ -54,7 +55,6 @@
       token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list}
   val mfix_delims: string -> string list
   val mfix_args: string -> int
-  val escape_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 *
@@ -229,7 +229,7 @@
 fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) [];
 val mfix_args = length o filter is_argument o read_mfix;
 
-val escape_mfix = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
+val escape = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
 
 end;