# HG changeset patch
# User wenzelm
# Date 1349811192 -7200
# Node ID 444cfaa331c9db09aa162f72a9739c7ed515eb23
# Parent  f27c96e9867262c6aac840fea22edb842fafaf26
clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;

diff -r f27c96e98672 -r 444cfaa331c9 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Oct 09 20:23:58 2012 +0200
+++ b/src/Pure/Isar/element.ML	Tue Oct 09 21:33:12 2012 +0200
@@ -493,9 +493,9 @@
   | init (Defines defs) = Context.map_proof (fn ctxt =>
       let
         val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
-        val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
-            let val ((c, _), t') = Local_Defs.cert_def ctxt t  (* FIXME adapt ps? *)
-            in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
+        val asms = defs' |> map (fn (b, (t, ps)) =>
+            let val (_, t') = Local_Defs.cert_def ctxt t  (* FIXME adapt ps? *)
+            in (t', (b, [(t', ps)])) end);
         val (_, ctxt') = ctxt
           |> fold Variable.auto_fixes (map #1 asms)
           |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
@@ -507,7 +507,13 @@
 
 fun activate_i elem ctxt =
   let
-    val elem' = map_ctxt_attrib Args.assignable elem;
+    val elem' =
+      (case map_ctxt_attrib Args.assignable elem of
+        Defines defs =>
+          Defines (defs |> map (fn ((a, atts), (t, ps)) =>
+            ((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt t)))) a, atts),
+              (t, ps))))
+      | e => e);
     val ctxt' = Context.proof_map (init elem') ctxt;
   in (map_ctxt_attrib Args.closure elem', ctxt') end;