# HG changeset patch
# User haftmann
# Date 1281445078 -7200
# Node ID e7e84919392bc5477f7cd8b986fc234a72e70d8f
# Parent  9dd57db3c0f25b352fcd2653852169cd825fe6b0
separated type from term parameters

diff -r 9dd57db3c0f2 -r e7e84919392b src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Aug 10 14:53:41 2010 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue Aug 10 14:57:58 2010 +0200
@@ -7,8 +7,8 @@
 
 signature GENERIC_TARGET =
 sig
-  val define: (((binding * typ) * mixfix) * (binding * term) -> term list
-    -> term list -> local_theory -> (term * thm) * local_theory)
+  val define: (((binding * typ) * mixfix) * (binding * term)
+    -> term list * term list -> local_theory -> (term * thm) * local_theory)
     -> (binding * mixfix) * (Attrib.binding * term) -> local_theory
     -> (term * (string * thm)) * local_theory
   val notes: (string
@@ -72,7 +72,7 @@
 
     (*foundation*)
     val ((lhs', global_def), lthy3) = foundation
-      (((b, U), mx'), (b_def, rhs')) params type_params lthy;
+      (((b, U), mx'), (b_def, rhs')) (type_params, term_params) lthy;
 
     (*local definition*)
     val ((lhs, local_def), lthy4) = lthy3
diff -r 9dd57db3c0f2 -r e7e84919392b src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Aug 10 14:53:41 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Tue Aug 10 14:57:58 2010 +0200
@@ -122,7 +122,7 @@
 fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
 
 fun foundation (ta as Target {target, is_locale, is_class, ...})
-    (((b, U), mx), (b_def, rhs')) params type_params lthy =
+    (((b, U), mx), (b_def, rhs')) (type_params, term_params) lthy =
   let
     val (mx1, mx2, mx3) = fork_mixfix ta mx;
     val (const, lthy2) = lthy |>
@@ -139,7 +139,7 @@
                 ##> Overloading.confirm b
           | NONE => Local_Theory.theory_result (Sign.declare_const ((b, U), mx3))));
     val Const (head, _) = const;
-    val lhs' = list_comb (const, params);
+    val lhs' = list_comb (const, type_params @ term_params);
   in
     lthy2
     |> pair lhs'