Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;

--- a/NEWS	Wed Mar 14 11:10:10 2012 +0100
+++ b/NEWS	Wed Mar 14 11:45:16 2012 +0100
@@ -371,6 +371,12 @@
 
 *** ML ***
 
+* Local_Theory.define no longer hard-wires default theorem name
+"foo_def": definitional packages need to make this explicit, and may
+choose to omit theorem bindings for definitions by using
+Binding.empty/Attrib.empty_binding.  Potential INCOMPATIBILITY for
+derived definitional packages.
+
 * Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in
 conformance with similar operations in structure Term and Logic.
 

--- a/src/Pure/Isar/generic_target.ML	Wed Mar 14 11:10:10 2012 +0100
+++ b/src/Pure/Isar/generic_target.ML	Wed Mar 14 11:45:16 2012 +0100
@@ -48,13 +48,11 @@
 
 (* define *)
 
-fun define foundation ((b, mx), ((proto_b_def, atts), rhs)) lthy =
+fun define foundation ((b, mx), ((b_def, atts), rhs)) lthy =
   let
     val thy = Proof_Context.theory_of lthy;
     val thy_ctxt = Proof_Context.init_global thy;
 
-    val b_def = Thm.def_binding_optional b proto_b_def;
-
     (*term and type parameters*)
     val crhs = Thm.cterm_of thy rhs;
     val ((defs, _), rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of;
@@ -202,7 +200,8 @@
     val lhs = list_comb (const, type_params @ term_params);
     val ((_, def), lthy3) = lthy2
       |> Local_Theory.background_theory_result
-        (Thm.add_def lthy2 false false (b_def, Logic.mk_equals (lhs, rhs)));
+        (Thm.add_def lthy2 false false
+          (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
   in ((lhs, def), lthy3) end;
 
 fun theory_notes kind global_facts lthy =

--- a/src/Pure/Isar/overloading.ML	Wed Mar 14 11:10:10 2012 +0100
+++ b/src/Pure/Isar/overloading.ML	Wed Mar 14 11:45:16 2012 +0100
@@ -147,15 +147,16 @@
   in 
     ctxt
     |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
-  end
+  end;
 
 fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
   Local_Theory.background_theory_result
     (Thm.add_def_global (not checked) true
-      (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
+      (Thm.def_binding_optional (Binding.name v) b_def,
+        Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
   ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
   ##> Local_Theory.target synchronize_syntax
-  #-> (fn (_, def) => pair (Const (c, U), def))
+  #-> (fn (_, def) => pair (Const (c, U), def));
 
 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   (case operation lthy b of