# HG changeset patch
# User wenzelm
# Date 1236113345 -3600
# Node ID b3f3ad327d4d56d3521dc42fa1104f643507cc42
# Parent  a2094a8c1672960686197eb0e87fafee3a931080
added @{binding} ML antiquotations;

diff -r a2094a8c1672 -r b3f3ad327d4d src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Tue Mar 03 21:48:40 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Tue Mar 03 21:49:05 2009 +0100
@@ -59,12 +59,13 @@
 
 
 
-(** concrete antiquotations **)
+(** misc antiquotations **)
 
 structure P = OuterParse;
 
-
-(* misc *)
+val _ = inline "binding" (Scan.lift (P.position Args.name) >> (fn b =>
+  ML_Syntax.atomic ("Binding.make " ^
+    ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position b)));
 
 val _ = value "theory"
   (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)