# HG changeset patch
# User haftmann
# Date 1281444442 -7200
# Node ID 228566e1ab00ed918adb9a22f05a40beb5c104f8
# Parent  9d4c0c74ae7d511544ca9ded7a3428fa61d69e65
name and argument grouping tuning

diff -r 9d4c0c74ae7d -r 228566e1ab00 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Aug 10 14:42:30 2010 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue Aug 10 14:47:22 2010 +0200
@@ -7,7 +7,7 @@
 
 signature GENERIC_TARGET =
 sig
-  val define: (((binding * typ) * mixfix) * term -> binding -> term list
+  val define: (((binding * typ) * mixfix) * (binding * term) -> term list
     -> (string * sort) list * term list -> local_theory -> (term * thm) * local_theory)
     -> (binding * mixfix) * (Attrib.binding * term) -> local_theory
     -> (term * (string * thm)) * local_theory
@@ -28,12 +28,12 @@
 
 (* define *)
 
-fun define foundation ((b, mx), ((name, atts), rhs)) lthy =
+fun define foundation ((b, mx), ((proto_b_def, atts), rhs)) lthy =
   let
     val thy = ProofContext.theory_of lthy;
     val thy_ctxt = ProofContext.init_global thy;
 
-    val name' = Thm.def_binding_optional b name;
+    val b_def = Thm.def_binding_optional b proto_b_def;
 
     (*term and type parameters*)
     val crhs = Thm.cterm_of thy rhs;
@@ -58,7 +58,7 @@
 
     (*foundation*)
     val ((lhs', global_def), lthy3) = foundation
-      (((b, U), mx), rhs') name' params (extra_tfrees, type_params) lthy;
+      (((b, U), mx), (b_def, rhs')) params (extra_tfrees, type_params) lthy;
 
     (*local definition*)
     val ((lhs, local_def), lthy4) = lthy3
@@ -70,7 +70,7 @@
 
     (*note*)
     val ([(res_name, [res])], lthy5) = lthy4
-      |> Local_Theory.notes_kind "" [((name', atts), [([def], [])])];
+      |> Local_Theory.notes_kind "" [((b_def, atts), [([def], [])])];
   in ((lhs, (res_name, res)), lthy5) end;
 
 
diff -r 9d4c0c74ae7d -r 228566e1ab00 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Aug 10 14:42:30 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Tue Aug 10 14:47:22 2010 +0200
@@ -141,7 +141,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), rhs') name' params (extra_tfrees, type_params) lthy =
+    (((b, U), mx), (b_def, rhs')) params (extra_tfrees, type_params) lthy =
   let
     val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx;
     val (const, lthy2) = lthy |>
@@ -164,11 +164,11 @@
     |> pair lhs'
     ||>> Local_Theory.theory_result
       (case Overloading.operation lthy b of
-        SOME (_, checked) => Overloading.define checked name' (head, rhs')
+        SOME (_, checked) => Overloading.define checked b_def (head, rhs')
       | NONE =>
           if is_some (Class_Target.instantiation_param lthy b)
-          then AxClass.define_overloaded name' (head, rhs')
-          else Thm.add_def false false (name', Logic.mk_equals (lhs', rhs')) #>> snd)
+          then AxClass.define_overloaded b_def (head, rhs')
+          else Thm.add_def false false (b_def, Logic.mk_equals (lhs', rhs')) #>> snd)
     ||> is_locale ? locale_const_declaration ta Syntax.mode_default ((b, mx2), lhs')
     ||> is_class ? class_target ta
           (Class_Target.declare target ((b, mx1), (type_params, lhs')))