Default names for definitions.

--- a/src/FOL/ex/NewLocaleTest.thy	Mon Dec 08 18:44:24 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Mon Dec 08 21:33:50 2008 +0100
@@ -121,7 +121,7 @@
     and lnot ("-- _" [60] 60)
   assumes assoc: "(x && y) && z = x && (y && z)"
     and notnot: "-- (-- x) = x"
-  defines lor_def: (* FIXME *) "x || y == --(-- x && -- y)"
+  defines "x || y == --(-- x && -- y)"
 begin
 
 lemma "x || y = --(-- x && --y)"

--- a/src/Pure/Isar/expression.ML	Mon Dec 08 18:44:24 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Mon Dec 08 21:33:50 2008 +0100
@@ -378,8 +378,11 @@
         (case elem of
           Assumes asms => Assumes (asms |> map (fn (a, propps) =>
             (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
-        | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
-            (a, (#2 (LocalDefs.cert_def ctxt (close_frees t)), no_binds ps))))
+        | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
+            let val ((c, _), t') = LocalDefs.cert_def ctxt (close_frees t)
+            in
+              ((Binding.map_base (Thm.def_name_optional c) name, atts), (t', no_binds ps))
+            end))
         | e => e)
       end;