# HG changeset patch
# User wenzelm
# Date 1176198923 -7200
# Node ID 6aa55c562ae7dfd01eb33c7e8a7ac89988ee1b2a
# Parent  c9e3de6dd8c2898c3a9754dad7d9ac7e91e80b76
inline_antiq: no longer forces ML_Syntax.atomic;

diff -r c9e3de6dd8c2 -r 6aa55c562ae7 src/Pure/Thy/ml_context.ML
--- a/src/Pure/Thy/ml_context.ML	Tue Apr 10 11:12:55 2007 +0200
+++ b/src/Pure/Thy/ml_context.ML	Tue Apr 10 11:55:23 2007 +0200
@@ -140,7 +140,7 @@
     fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names)
       | expand (Antiquote.Antiq x) names =
           (case command (Antiquote.scan_arguments (! global_lexicon) antiq x) of
-            Inline s => (("", ML_Syntax.atomic s), names)
+            Inline s => (("", s), names)
           | Value (a, s) =>
               let
                 val a' = if ML_Syntax.is_identifier a then a else "val";
@@ -189,9 +189,9 @@
 
 val _ = value_antiq "context" (Scan.succeed ("context", "ML_Context.the_local_context ()"));
 
-val _ = inline_antiq "typ" (Args.typ >> ML_Syntax.print_typ);
-val _ = inline_antiq "term" (Args.term >> ML_Syntax.print_term);
-val _ = inline_antiq "prop" (Args.prop >> ML_Syntax.print_term);
+val _ = inline_antiq "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
+val _ = inline_antiq "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
+val _ = inline_antiq "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
 
 val _ = value_antiq "ctyp" (Args.typ >> (fn T =>
   ("ctyp",