src/Pure/type.ML
changeset 8715 2cdabe1bb350
parent 8610 f0f7600b2605
child 8721 453b493ece0a
--- a/src/Pure/type.ML	Fri Apr 14 16:12:46 2000 +0200
+++ b/src/Pure/type.ML	Fri Apr 14 17:29:57 2000 +0200
@@ -29,6 +29,7 @@
   val defaultS: type_sig -> sort
   val logical_types: type_sig -> string list
   val univ_witness: type_sig -> (typ * sort) option
+  val is_type_abbr: type_sig -> string -> bool
   val subsort: type_sig -> sort * sort -> bool
   val eq_sort: type_sig -> sort * sort -> bool
   val norm_sort: type_sig -> sort -> sort
@@ -178,6 +179,7 @@
 fun defaultS (TySg {default, ...}) = default;
 fun logical_types (TySg {log_types, ...}) = log_types;
 fun univ_witness (TySg {univ_witness, ...}) = univ_witness;
+fun is_type_abbr (TySg {abbrs, ...}) name = is_some (Symtab.lookup (abbrs, name));
 
 
 (* sorts *)