clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional;
clarified Generic_Target.define: avoid duplicate def binding via Local_Defs.add_def;

--- a/src/Pure/Isar/local_defs.ML	Tue Oct 09 19:24:19 2012 +0200
+++ b/src/Pure/Isar/local_defs.ML	Tue Oct 09 20:05:17 2012 +0200
@@ -89,16 +89,14 @@
 fun add_defs defs ctxt =
   let
     val ((xs, mxs), specs) = defs |> split_list |>> split_list;
-    val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
-    val names = map2 Thm.def_binding_optional xs bfacts;
+    val (bs, rhss) = specs |> split_list;
     val eqs = mk_def ctxt (xs ~~ rhss);
     val lhss = map (fst o Logic.dest_equals) eqs;
   in
     ctxt
     |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2
     |> fold Variable.declare_term eqs
-    |> Proof_Context.add_assms_i def_export
-      (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
+    |> Proof_Context.add_assms_i def_export (map2 (fn b => fn eq => (b, [(eq, [])])) bs eqs)
     |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
   end;
 

--- a/src/Pure/Isar/proof.ML	Tue Oct 09 19:24:19 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Oct 09 20:05:17 2012 +0200
@@ -643,7 +643,11 @@
     |>> map (fn (x, _, mx) => (x, mx))
     |-> (fn vars =>
       map_context_result (prep_binds false (map swap raw_rhss))
-      #-> (fn rhss => map_context_result (Local_Defs.add_defs (vars ~~ (name_atts ~~ rhss)))))
+      #-> (fn rhss =>
+        let
+          val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
+            ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
+        in map_context_result (Local_Defs.add_defs defs) end))
     |-> (set_facts o map (#2 o #2))
   end;
 

--- a/src/Tools/induct.ML	Tue Oct 09 19:24:19 2012 +0200
+++ b/src/Tools/induct.ML	Tue Oct 09 20:05:17 2012 +0200
@@ -705,15 +705,15 @@
     fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt)
       | add (SOME (SOME x, (t, _))) ctxt =
           let val ([(lhs, (_, th))], ctxt') =
-            Local_Defs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
+            Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt
           in ((SOME lhs, [th]), ctxt') end
       | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
       | add (SOME (NONE, (t, _))) ctxt =
           let
             val (s, _) = Name.variant "x" (Variable.names_of ctxt);
-            val ([(lhs, (_, th))], ctxt') =
-              Local_Defs.add_defs [((Binding.name s, NoSyn),
-                (Thm.empty_binding, t))] ctxt
+            val x = Binding.name s;
+            val ([(lhs, (_, th))], ctxt') = ctxt
+              |> Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))];
           in ((SOME lhs, [th]), ctxt') end
       | add NONE ctxt = ((NONE, []), ctxt);
   in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;