1.1 --- a/src/Pure/Isar/class_target.ML	Sun Mar 21 06:59:23 2010 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Sun Mar 21 08:46:49 2010 +0100
     1.3 @@ -16,12 +16,13 @@
     1.4    val rules: theory -> class -> thm option * thm
     1.5    val these_params: theory -> sort -> (string * (class * (string * typ))) list
     1.6    val these_defs: theory -> sort -> thm list
     1.7 -  val these_operations: theory -> sort -> (string * (class * (typ * term))) list
     1.8 +  val these_operations: theory -> sort
     1.9 +    -> (string * (class * (typ * term))) list
    1.10    val print_classes: theory -> unit
    1.11  
    1.12    val begin: class list -> sort -> Proof.context -> Proof.context
    1.13    val init: class -> theory -> Proof.context
    1.14 -  val declare: class -> (binding * mixfix) * term -> theory -> theory
    1.15 +  val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory
    1.16    val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
    1.17    val class_prefix: string -> string
    1.18    val refresh_syntax: class -> Proof.context -> Proof.context
    1.19 @@ -253,8 +254,8 @@
    1.20  
    1.21  (* class context syntax *)
    1.22  
    1.23 -fun these_unchecks thy =
    1.24 -  map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy;
    1.25 +fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
    1.26 +  o these_operations thy;
    1.27  
    1.28  fun redeclare_const thy c =
    1.29    let val b = Long_Name.base_name c
    1.30 @@ -317,15 +318,15 @@
    1.31  
    1.32  val class_prefix = Logic.const_of_class o Long_Name.base_name;
    1.33  
    1.34 -fun declare class ((c, mx), dict) thy =
    1.35 +fun declare class ((c, mx), (type_params, dict)) thy =
    1.36    let
    1.37      val morph = morphism thy class;
    1.38      val b = Morphism.binding morph c;
    1.39      val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b);
    1.40      val c' = Sign.full_name thy b;
    1.41      val dict' = Morphism.term morph dict;
    1.42 -    val ty' = Term.fastype_of dict';
    1.43 -    val def_eq = Logic.mk_equals (Const (c', ty'), dict')
    1.44 +    val ty' = map Term.fastype_of type_params ---> Term.fastype_of dict';
    1.45 +    val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), type_params), dict')
    1.46        |> map_types Type.strip_sorts;
    1.47    in
    1.48      thy
    1.49 @@ -335,7 +336,7 @@
    1.50      |>> Thm.varifyT_global
    1.51      |-> (fn def_thm => PureThy.store_thm (b_def, def_thm)
    1.52        #> snd
    1.53 -      #> register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
    1.54 +      #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
    1.55      |> Sign.add_const_constraint (c', SOME ty')
    1.56    end;
    1.57  

     2.1 --- a/src/Pure/Isar/theory_target.ML	Sun Mar 21 06:59:23 2010 +0100
     2.2 +++ b/src/Pure/Isar/theory_target.ML	Sun Mar 21 08:46:49 2010 +0100
     2.3 @@ -277,7 +277,7 @@
     2.4    in
     2.5      lthy'
     2.6      |> is_locale ? syntax_declaration ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
     2.7 -    |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
     2.8 +    |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), (type_params, t)))
     2.9      |> Local_Defs.add_def ((b, NoSyn), t)
    2.10    end;
    2.11