added simple_str_of_sort;
authorwenzelm
Mon, 06 Oct 1997 18:39:25 +0200
changeset 3782 c1b4be0e77cb
parent 3781 ec519ba6196e
child 3783 37fb4f64eb9d
added simple_str_of_sort;
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);