# HG changeset patch
# User wenzelm
# Date 1206374973 -3600
# Node ID b615c10404bf82447f74303e65f6845920050e91
# Parent  f882403f0d5605bb5dc0301136e147ad036172ce
removed unused print_properties, print_position;

diff -r f882403f0d56 -r b615c10404bf src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Mon Mar 24 16:05:25 2008 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Mon Mar 24 17:09:33 2008 +0100
@@ -19,8 +19,6 @@
   val print_char: string -> string
   val print_string: string -> string
   val print_strings: string list -> string
-  val print_properties: Markup.property list -> string
-  val print_position: Position.T -> string
   val print_indexname: indexname -> string
   val print_class: class -> string
   val print_sort: sort -> string
@@ -71,9 +69,6 @@
 val print_string = quote o translate_string print_char;
 val print_strings = print_list print_string;
 
-val print_properties = print_list (print_pair print_string print_string);
-fun print_position pos = "Position.of_properties " ^ print_properties (Position.properties_of pos);
-
 val print_indexname = print_pair print_string print_int;
 
 val print_class = print_string;