allow qualified names;
authorwenzelm
Thu, 03 Jun 2010 22:06:37 +0200
changeset 37304645f849eefa7
parent 37303 0e4c721d4567
child 37305 9763792e4ac7
allow qualified names;
src/Pure/ML/ml_antiquote.ML
     1.1 --- a/src/Pure/ML/ml_antiquote.ML	Thu Jun 03 16:56:44 2010 +0200
     1.2 +++ b/src/Pure/ML/ml_antiquote.ML	Thu Jun 03 22:06:37 2010 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4  fun declaration kind name scan = ML_Context.add_antiq name
     1.5    (fn _ => scan >> (fn s => fn background =>
     1.6      let
     1.7 -      val (a, background') = variant name background;
     1.8 +      val (a, background') = variant (translate_string (fn "." => "_" | c => c) name) background;
     1.9        val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
    1.10        val body = "Isabelle." ^ a;
    1.11      in (K (env, body), background') end));