# HG changeset patch
# User wenzelm
# Date 1275595597 -7200
# Node ID 645f849eefa7bbb6f8ba9c741a000033b1b649d7
# Parent  0e4c721d45678a749a0899330efc8244653ca45f
allow qualified names;

diff -r 0e4c721d4567 -r 645f849eefa7 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Thu Jun 03 16:56:44 2010 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Thu Jun 03 22:06:37 2010 +0200
@@ -46,7 +46,7 @@
 fun declaration kind name scan = ML_Context.add_antiq name
   (fn _ => scan >> (fn s => fn background =>
     let
-      val (a, background') = variant name background;
+      val (a, background') = variant (translate_string (fn "." => "_" | c => c) name) background;
       val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
       val body = "Isabelle." ^ a;
     in (K (env, body), background') end));