added simple_str_of_sort;
authorwenzelm
Mon Oct 06 18:39:25 1997 +0200 (1997-10-06)
changeset 3782c1b4be0e77cb
parent 3781 ec519ba6196e
child 3783 37fb4f64eb9d
added simple_str_of_sort;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Mon Oct 06 18:29:43 1997 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Oct 06 18:39:25 1997 +0200
     1.3 @@ -53,6 +53,7 @@
     1.4    val pretty_term: syntax -> bool -> term -> Pretty.T
     1.5    val pretty_typ: syntax -> typ -> Pretty.T
     1.6    val pretty_sort: syntax -> sort -> Pretty.T
     1.7 +  val simple_str_of_sort: sort -> string
     1.8    val simple_string_of_typ: typ -> string
     1.9    val simple_pprint_typ: typ -> pprint_args -> unit
    1.10    val ambiguity_level: int ref
    1.11 @@ -458,6 +459,7 @@
    1.12  fun pretty_typ syn = pretty_t typ_to_ast pretty_typ_ast syn false;
    1.13  fun pretty_sort syn = pretty_t sort_to_ast pretty_typ_ast syn false;
    1.14  
    1.15 +val simple_str_of_sort = Pretty.str_of o pretty_sort type_syn;
    1.16  val simple_string_of_typ = Pretty.string_of o (pretty_typ type_syn);
    1.17  val simple_pprint_typ = Pretty.pprint o Pretty.quote o (pretty_typ type_syn);
    1.18