added make_binding;
authorwenzelm
Sun, 15 Mar 2009 15:59:42 +0100
changeset 30523 4007ea1ddac2
parent 30522 e26b80647189
child 30524 92af4e8c54a6
added make_binding;
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;