# HG changeset patch
# User wenzelm
# Date 769963508 -7200
# Node ID 324ad2e028260e2fc0425a42804c4b19f098a90d
# Parent  3c2c40c87112c9ca7dc9fb1537aadee8837fbf90
replaced "logic" by logicC;
added subsort, norm_sort;

diff -r 3c2c40c87112 -r 324ad2e02826 src/Pure/type.ML
--- a/src/Pure/type.ML	Thu May 26 16:43:48 1994 +0200
+++ b/src/Pure/type.ML	Thu May 26 16:45:08 1994 +0200
@@ -21,6 +21,8 @@
      abbrs: (string * (indexname list * typ)) list,
      coreg: (string * (class * sort list) list) list}
   val defaultS: type_sig -> sort
+  val subsort: type_sig -> sort * sort -> bool
+  val norm_sort: type_sig -> sort -> sort
   val logical_types: type_sig -> string list
   val tsig0: type_sig
   val extend_tsig: type_sig ->
@@ -135,7 +137,7 @@
    a class which is a subclass of "logic" *)
 
 fun logical_type(tsig as TySg{subclass, coreg, ...}) t =
-  let fun is_log C = leq subclass (C, "logic")
+  let fun is_log C = leq subclass (C, logicC)
   in case assoc (coreg, t) of
       Some(ars) => exists (is_log o #1) ars
     | None => err_undcl_type(t)
@@ -331,6 +333,15 @@
     coreg = []};
 
 
+(* sorts *)
+
+fun norm_sort (TySg {subclass, ...}) S =
+  sort_strings (min_sort subclass S);
+
+fun subsort (TySg {subclass, ...}) (S1, S2) =
+  sortorder subclass (S1, S2);
+
+
 fun not_ident(s) = error("Must be an identifier: " ^ s);
 
 fun twice(a) = error("Type constructor " ^a^ " has already been declared.");