# HG changeset patch
# User wenzelm
# Date 955726197 -7200
# Node ID 2cdabe1bb35010e62f18d9b8f6dc52e8242dda9e
# Parent  61cafd91963c56b1776f8fa4b2897718b728065f
added is_type_abbr;

diff -r 61cafd91963c -r 2cdabe1bb350 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Apr 14 16:12:46 2000 +0200
+++ b/src/Pure/sign.ML	Fri Apr 14 17:29:57 2000 +0200
@@ -47,6 +47,7 @@
   val of_sort: sg -> typ * sort -> bool
   val witness_sorts: sg -> sort list -> sort list -> (typ * sort) list
   val univ_witness: sg -> (typ * sort) option
+  val is_type_abbr: sg -> string -> bool
   val classK: string
   val typeK: string
   val constK: string
@@ -267,6 +268,7 @@
 val of_sort = Type.of_sort o tsig_of;
 val witness_sorts = Type.witness_sorts o tsig_of;
 val univ_witness = Type.univ_witness o tsig_of;
+val is_type_abbr = Type.is_type_abbr o tsig_of;
 
 
 
diff -r 61cafd91963c -r 2cdabe1bb350 src/Pure/type.ML
--- 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 *)