1.1 --- a/src/Pure/ML/ml_antiquote.ML	Sat Feb 06 23:26:17 2010 +0100
     1.2 +++ b/src/Pure/ML/ml_antiquote.ML	Sun Feb 07 18:04:48 2010 +0100
     1.3 @@ -38,17 +38,17 @@
     1.4  
     1.5  fun macro name scan = ML_Context.add_antiq name
     1.6    (fn _ => scan :|-- (fn ctxt => Scan.depend (fn _ => Scan.succeed
     1.7 -    (Context.Proof ctxt, fn {background, ...} => (K ("", ""), background)))));
     1.8 +    (Context.Proof ctxt, fn background => (K ("", ""), background)))));
     1.9  
    1.10  fun inline name scan = ML_Context.add_antiq name
    1.11 -  (fn _ => scan >> (fn s => fn {background, ...} => (K ("", s), background)));
    1.12 +  (fn _ => scan >> (fn s => fn background => (K ("", s), background)));
    1.13  
    1.14  fun declaration kind name scan = ML_Context.add_antiq name
    1.15 -  (fn _ => scan >> (fn s => fn {struct_name, background} =>
    1.16 +  (fn _ => scan >> (fn s => fn background =>
    1.17      let
    1.18        val (a, background') = variant name background;
    1.19        val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
    1.20 -      val body = struct_name ^ "." ^ a;
    1.21 +      val body = "Isabelle." ^ a;
    1.22      in (K (env, body), background') end));
    1.23  
    1.24  val value = declaration "val";