more robust ML_Antiquote.variant via Name.desymbolize (which also allows symbolic names, for example);

--- a/src/Pure/ML/ml_antiquote.ML	Fri Aug 23 19:53:27 2013 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Fri Aug 23 20:09:34 2013 +0200
@@ -29,7 +29,7 @@
 fun variant a ctxt =
   let
     val names = Names.get ctxt;
-    val (b, names') = Name.variant a names;
+    val (b, names') = Name.variant (Name.desymbolize false a) names;
     val ctxt' = Names.put names' ctxt;
   in (b, ctxt') end;
 
@@ -45,8 +45,7 @@
     (Scan.depend (fn context => Scan.pass context scan >> (fn s =>
       let
         val ctxt = Context.the_proof context;
-        val (a, ctxt') =
-          variant (translate_string (fn "." => "_" | c => c) (Binding.name_of name)) ctxt;
+        val (a, ctxt') = variant (Binding.name_of name) ctxt;
         val env = "val " ^ a ^ " = " ^ s ^ ";\n";
         val body = "Isabelle." ^ a;
       in (Context.Proof ctxt', (K (env, body))) end)));