--- 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
--- 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'