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

     2.1 --- a/src/Pure/logic.ML	Sun Mar 21 19:30:19 2010 +0100
     2.2 +++ b/src/Pure/logic.ML	Sun Mar 21 22:13:31 2010 +0100
     2.3 @@ -38,6 +38,7 @@
     2.4    val class_of_const: string -> class
     2.5    val mk_of_class: typ * class -> term
     2.6    val dest_of_class: term -> typ * class
     2.7 +  val mk_of_sort: typ * sort -> term list
     2.8    val name_classrel: string * string -> string
     2.9    val mk_classrel: class * class -> term
    2.10    val dest_classrel: term -> class * class
    2.11 @@ -217,7 +218,7 @@
    2.12    handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
    2.13  
    2.14  
    2.15 -(* class membership *)
    2.16 +(* class/sort membership *)
    2.17  
    2.18  fun mk_of_class (ty, c) =
    2.19    Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
    2.20 @@ -225,6 +226,8 @@
    2.21  fun dest_of_class (Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
    2.22    | dest_of_class t = raise TERM ("dest_of_class", [t]);
    2.23  
    2.24 +fun mk_of_sort (ty, S) = map (fn c => mk_of_class (ty, c)) S;
    2.25 +
    2.26  
    2.27  (* class relations *)
    2.28  

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