# HG changeset patch
# User wenzelm
# Date 1204377014 -3600
# Node ID 9cb1b484fe9639c62b1cb6229574620cc52923b3
# Parent  3e099fc47afd61953f3784c18e18a076f578a7ef
added @{const} antiquotation;

diff -r 3e099fc47afd -r 9cb1b484fe96 NEWS
--- a/NEWS	Sat Mar 01 14:10:13 2008 +0100
+++ b/NEWS	Sat Mar 01 14:10:14 2008 +0100
@@ -112,6 +112,9 @@
 
 *** ML ***
 
+* ML within Isar: antiquotation @{const name} or @{const
+name(typargs)} produces statically-checked Const term.
+
 * The ``print mode'' is now a thread-local value derived from a global
 template (the former print_mode reference), thus access becomes
 non-critical.  The global print_mode reference is for session
diff -r 3e099fc47afd -r 9cb1b484fe96 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Sat Mar 01 14:10:13 2008 +0100
+++ b/src/Pure/ML/ml_context.ML	Sat Mar 01 14:10:14 2008 +0100
@@ -251,6 +251,15 @@
 val _ = inline_antiq "const_name" (const false);
 val _ = inline_antiq "const_syntax" (const true);
 
+val _ = inline_antiq "const"
+  ((Scan.state >> Context.proof_of) -- Scan.lift Args.name --
+    Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) []
+    >> (fn ((ctxt, c), Ts) =>
+      let
+        val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c);
+        val T = Consts.instance (ProofContext.consts_of ctxt) (c, Ts);
+      in ML_Syntax.atomic (ML_Syntax.print_term (Const (c, T))) end));
+
 in val _ = () end;