# HG changeset patch
# User wenzelm
# Date 1238013349 -3600
# Node ID 0579dec9f8bad9d0c5d854e07d0e0d64d9e9e777
# Parent  6d8dcfb264dcacd500da7ed13afe39a4a17ec6e8
@{binding} is not a constructor term and should not be inlined, otherwise we loose value polymorphism;

diff -r 6d8dcfb264dc -r 0579dec9f8ba src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Wed Mar 25 21:34:31 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Wed Mar 25 21:35:49 2009 +0100
@@ -59,7 +59,7 @@
 
 structure P = OuterParse;
 
-val _ = inline "binding"
+val _ = value "binding"
   (Scan.lift (P.position Args.name) >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
 
 val _ = value "theory"