# HG changeset patch
# User haftmann
# Date 1269157609 -3600
# Node ID 0d394a82337ed8979989b45079c41b7002cd6ca1
# Parent  2ae4b758550180311e0232a21ab6ec8862912ada
handle hidden polymorphism in class target (without class target syntax, though)

diff -r 2ae4b7585501 -r 0d394a82337e src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Sun Mar 21 06:59:23 2010 +0100
+++ b/src/Pure/Isar/class_target.ML	Sun Mar 21 08:46:49 2010 +0100
@@ -16,12 +16,13 @@
   val rules: theory -> class -> thm option * thm
   val these_params: theory -> sort -> (string * (class * (string * typ))) list
   val these_defs: theory -> sort -> thm list
-  val these_operations: theory -> sort -> (string * (class * (typ * term))) list
+  val these_operations: theory -> sort
+    -> (string * (class * (typ * term))) list
   val print_classes: theory -> unit
 
   val begin: class list -> sort -> Proof.context -> Proof.context
   val init: class -> theory -> Proof.context
-  val declare: class -> (binding * mixfix) * term -> theory -> theory
+  val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory
   val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
   val class_prefix: string -> string
   val refresh_syntax: class -> Proof.context -> Proof.context
@@ -253,8 +254,8 @@
 
 (* class context syntax *)
 
-fun these_unchecks thy =
-  map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy;
+fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
+  o these_operations thy;
 
 fun redeclare_const thy c =
   let val b = Long_Name.base_name c
@@ -317,15 +318,15 @@
 
 val class_prefix = Logic.const_of_class o Long_Name.base_name;
 
-fun declare class ((c, mx), dict) thy =
+fun declare class ((c, mx), (type_params, dict)) thy =
   let
     val morph = morphism thy class;
     val b = Morphism.binding morph c;
     val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b);
     val c' = Sign.full_name thy b;
     val dict' = Morphism.term morph dict;
-    val ty' = Term.fastype_of dict';
-    val def_eq = Logic.mk_equals (Const (c', ty'), dict')
+    val ty' = map Term.fastype_of type_params ---> Term.fastype_of dict';
+    val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), type_params), dict')
       |> map_types Type.strip_sorts;
   in
     thy
@@ -335,7 +336,7 @@
     |>> Thm.varifyT_global
     |-> (fn def_thm => PureThy.store_thm (b_def, def_thm)
       #> snd
-      #> register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
+      #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
     |> Sign.add_const_constraint (c', SOME ty')
   end;
 
diff -r 2ae4b7585501 -r 0d394a82337e src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sun Mar 21 06:59:23 2010 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sun Mar 21 08:46:49 2010 +0100
@@ -277,7 +277,7 @@
   in
     lthy'
     |> is_locale ? syntax_declaration ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
-    |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
+    |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), (type_params, t)))
     |> Local_Defs.add_def ((b, NoSyn), t)
   end;