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