# HG changeset patch
# User wenzelm
# Date 1176488598 -7200
# Node ID 73517244fc46a032a8e40acfc98f6b5cceaf6453
# Parent  3e492ba593551688d16fe44e89465bedde534a96
eval_antiquotes: proper parentheses for projection;

diff -r 3e492ba59355 -r 73517244fc46 src/Pure/Thy/ml_context.ML
--- a/src/Pure/Thy/ml_context.ML	Fri Apr 13 16:40:16 2007 +0200
+++ b/src/Pure/Thy/ml_context.ML	Fri Apr 13 20:23:18 2007 +0200
@@ -148,7 +148,11 @@
               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", f ^ " Isabelle." ^ b), names') end);
+                val binding = "val " ^ b ^ " = " ^ s ^ ";\n";
+                val value =
+                  if f = "" then "Isabelle." ^ b
+                  else "(" ^ f ^ " Isabelle." ^ b ^ ")";
+              in ((binding, value), names') end);
 
     val (decls, body) =
       fold_map expand ants ML_Syntax.reserved