diff -r 5ab11152daeb -r c90a3b98473e src/Pure/Thy/ml_context.ML
--- a/src/Pure/Thy/ml_context.ML	Thu Apr 12 23:06:25 2007 +0200
+++ b/src/Pure/Thy/ml_context.ML	Thu Apr 12 23:06:27 2007 +0200
@@ -29,6 +29,8 @@
     (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
   val value_antiq: string ->
     (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit
+  val proj_value_antiq: string -> (Context.generic * Args.T list ->
+      (string * string * string) * (Context.generic * Args.T list)) -> unit
   val use_mltext: string -> bool -> Context.generic option -> unit
   val use_mltext_update: string -> bool -> Context.generic -> Context.generic
   val use_let: string -> string -> string -> Context.generic -> Context.generic
@@ -83,7 +85,7 @@
 
 (* maintain commands *)
 
-datatype antiq = Inline of string | Value of string * string;
+datatype antiq = Inline of string | ProjValue of string * string * string;
 val global_parsers = ref (Symtab.empty:
   (Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) Symtab.table);
 
@@ -97,7 +99,8 @@
 in
 
 val inline_antiq = add_item Inline;
-val value_antiq = add_item Value;
+val proj_value_antiq = add_item ProjValue;
+fun value_antiq name scan = proj_value_antiq name (scan >> (fn (a, s) => (a, s, "")));
 
 end;
 
@@ -141,11 +144,11 @@
       | expand (Antiquote.Antiq x) names =
           (case command (Antiquote.scan_arguments (! global_lexicon) antiq x) of
             Inline s => (("", s), names)
-          | Value (a, s) =>
+          | ProjValue (a, s, f) =>
               let
                 val a' = if ML_Syntax.is_identifier a then a else "val";
                 val ([b], names') = Name.variants [a'] names;
-              in (("val " ^ b ^ " = " ^ s ^ ";\n", "Isabelle." ^ b), names') end);
+              in (("val " ^ b ^ " = " ^ s ^ ";\n", f ^ " Isabelle." ^ b), names') end);
 
     val (decls, body) =
       fold_map expand ants ML_Syntax.reserved