src/Pure/logic.ML
changeset 35854 d452abc96459
parent 35845 e5980f0ad025
child 36767 d0095729e1f1
     1.1 --- a/src/Pure/logic.ML	Sun Mar 21 19:30:19 2010 +0100
     1.2 +++ b/src/Pure/logic.ML	Sun Mar 21 22:13:31 2010 +0100
     1.3 @@ -38,6 +38,7 @@
     1.4    val class_of_const: string -> class
     1.5    val mk_of_class: typ * class -> term
     1.6    val dest_of_class: term -> typ * class
     1.7 +  val mk_of_sort: typ * sort -> term list
     1.8    val name_classrel: string * string -> string
     1.9    val mk_classrel: class * class -> term
    1.10    val dest_classrel: term -> class * class
    1.11 @@ -217,7 +218,7 @@
    1.12    handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
    1.13  
    1.14  
    1.15 -(* class membership *)
    1.16 +(* class/sort membership *)
    1.17  
    1.18  fun mk_of_class (ty, c) =
    1.19    Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
    1.20 @@ -225,6 +226,8 @@
    1.21  fun dest_of_class (Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
    1.22    | dest_of_class t = raise TERM ("dest_of_class", [t]);
    1.23  
    1.24 +fun mk_of_sort (ty, S) = map (fn c => mk_of_class (ty, c)) S;
    1.25 +
    1.26  
    1.27  (* class relations *)
    1.28