Logic.mk_of_sort convenience;

--- a/src/Pure/axclass.ML	Sun Mar 21 19:30:19 2010 +0100
+++ b/src/Pure/axclass.ML	Sun Mar 21 22:13:31 2010 +0100
@@ -467,7 +467,7 @@
 
     (* definition *)
 
-    val conjs = map (curry Logic.mk_of_class (Term.aT [])) super @ flat axiomss;
+    val conjs = Logic.mk_of_sort (Term.aT [], super) @ flat axiomss;
     val class_eq =
       Logic.mk_equals (Logic.mk_of_class (Term.aT [], class), Logic.mk_conjunction_balanced conjs);
 

--- 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 *)
 

--- a/src/Pure/thm.ML	Sun Mar 21 19:30:19 2010 +0100
+++ b/src/Pure/thm.ML	Sun Mar 21 22:13:31 2010 +0100
@@ -1231,7 +1231,7 @@
       raise THM ("unconstrainT: not a type variable", 0, [th]);
     val T' = TVar ((x, i), []);
     val unconstrain = Term.map_types (Term.map_atyps (fn U => if U = T then T' else U));
-    val constraints = map (curry Logic.mk_of_class T') S;
+    val constraints = Logic.mk_of_sort (T', S);
   in
     Thm (deriv_rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])),
      {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),