diff -r 4b2eccaec3f6 -r e7ea35b41e2d src/Pure/Isar/generic_target.ML
--- 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 =