--- a/src/Pure/logic.ML Sun Mar 21 19:30:19 2010 +0100
+++ b/src/Pure/logic.ML Sun Mar 21 22:13:31 2010 +0100
@@ -38,6 +38,7 @@
val class_of_const: string -> class
val mk_of_class: typ * class -> term
val dest_of_class: term -> typ * class
+ val mk_of_sort: typ * sort -> term list
val name_classrel: string * string -> string
val mk_classrel: class * class -> term
val dest_classrel: term -> class * class
@@ -217,7 +218,7 @@
handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
-(* class membership *)
+(* class/sort membership *)
fun mk_of_class (ty, c) =
Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
@@ -225,6 +226,8 @@
fun dest_of_class (Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
| dest_of_class t = raise TERM ("dest_of_class", [t]);
+fun mk_of_sort (ty, S) = map (fn c => mk_of_class (ty, c)) S;
+
(* class relations *)