tuned signature

--- a/src/Pure/Isar/class.ML	Thu May 22 16:59:49 2014 +0200
+++ b/src/Pure/Isar/class.ML	Thu May 22 16:59:49 2014 +0200
@@ -17,7 +17,7 @@
   val print_classes: Proof.context -> unit
   val init: class -> theory -> Proof.context
   val begin: class list -> sort -> Proof.context -> Proof.context
-  val const: class -> (binding * mixfix) * (term list * term list * term) -> local_theory -> local_theory
+  val const: class -> (binding * mixfix) * term -> term list * term list -> local_theory -> local_theory
   val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
   val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
   val class_prefix: string -> string
@@ -320,7 +320,7 @@
   Local_Theory.raw_theory f
   #> synchronize_class_syntax_target class;
 
-fun target_const class ((c, mx), (type_params, term_params, dict)) thy =
+fun target_const class ((c, mx), dict) (type_params, term_params) thy =
   let
     val morph = morphism thy class;
     val class_params = map fst (these_params thy [class]);
@@ -366,7 +366,7 @@
 
 in
 
-fun const class arg = target_extension (target_const class arg) class;
+fun const class arg params = target_extension (target_const class arg params) class;
 fun abbrev class prmode arg = target_extension (target_abbrev class prmode arg) class;
 
 end;

--- a/src/Pure/Isar/named_target.ML	Thu May 22 16:59:49 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Thu May 22 16:59:49 2014 +0200
@@ -103,7 +103,7 @@
 fun class_foundation target (((b, U), mx), (b_def, rhs)) params =
   Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params
   #-> (fn (lhs, def) => class_const target Syntax.mode_default (b, lhs)
-    #> Class.const target ((b, mx), (#1 params, #2 params, lhs))
+    #> Class.const target ((b, mx), lhs) params
     #> pair (lhs, def));
 
 fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =