# HG changeset patch
# User wenzelm
# Date 1237129182 -3600
# Node ID 4007ea1ddac28dcf409618da131fd79443cf4670
# Parent  e26b806471897b5e849529cdf884ea268017687b
added make_binding;

diff -r e26b80647189 -r 4007ea1ddac2 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Sat Mar 14 00:13:50 2009 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Sun Mar 15 15:59:42 2009 +0100
@@ -20,6 +20,7 @@
   val print_strings: string list -> string
   val print_properties: Properties.T -> string
   val print_position: Position.T -> string
+  val make_binding: string * Position.T -> string
   val print_indexname: indexname -> string
   val print_class: class -> string
   val print_sort: sort -> string
@@ -72,6 +73,7 @@
 
 val print_properties = print_list (print_pair print_string print_string);
 fun print_position pos = "Position.of_properties " ^ print_properties (Position.properties_of pos);
+fun make_binding (name, pos) = "Binding.make " ^ print_pair print_string print_position (name, pos);
 
 val print_indexname = print_pair print_string print_int;