# HG changeset patch
# User wenzelm
# Date 876155965 -7200
# Node ID c1b4be0e77cba6d3749edb2a83d7c9efc70e33ce
# Parent  ec519ba6196ebb0c68063f90b6a27eefcac46b4a
added simple_str_of_sort;

diff -r ec519ba6196e -r c1b4be0e77cb src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Oct 06 18:29:43 1997 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Oct 06 18:39:25 1997 +0200
@@ -53,6 +53,7 @@
   val pretty_term: syntax -> bool -> term -> Pretty.T
   val pretty_typ: syntax -> typ -> Pretty.T
   val pretty_sort: syntax -> sort -> Pretty.T
+  val simple_str_of_sort: sort -> string
   val simple_string_of_typ: typ -> string
   val simple_pprint_typ: typ -> pprint_args -> unit
   val ambiguity_level: int ref
@@ -458,6 +459,7 @@
 fun pretty_typ syn = pretty_t typ_to_ast pretty_typ_ast syn false;
 fun pretty_sort syn = pretty_t sort_to_ast pretty_typ_ast syn false;
 
+val simple_str_of_sort = Pretty.str_of o pretty_sort type_syn;
 val simple_string_of_typ = Pretty.string_of o (pretty_typ type_syn);
 val simple_pprint_typ = Pretty.pprint o Pretty.quote o (pretty_typ type_syn);