src/Pure/Isar/locale.ML

       |> ProofContext.add_syntax fixes
   | activate (ctxt, Assumes asms) =
       ctxt |> ProofContext.fix_frees (flat (map (map #1 o #2) asms))
       |> ProofContext.assume_i ProofContext.export_assume asms |> #1
   | activate (ctxt, Defines defs) = #1 (ProofContext.assume_i ProofContext.export_def
-      (map (fn (a, (t, ps)) => (a, [(ProofContext.cert_def ctxt t, (ps, []))])) defs) ctxt)
+      (map (fn ((name, atts), (t, ps)) =>
+        let val (c, t') = ProofContext.cert_def ctxt t
+        in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end) defs) ctxt)
   | activate (ctxt, Notes facts) = #1 (ProofContext.have_thmss facts ctxt)
   | activate (ctxt, Uses name) = activate_locale_i name ctxt
 
 and activate_elements_i elems ctxt = foldl activate (ctxt, elems)
 

       | prt_elem (Notes facts) = Pretty.big_list "notes" (map prt_fact facts)
       | prt_elem (Uses name) = Pretty.str ("uses " ^ cond_extern sg name);
 
     val prt_header = Pretty.block (Pretty.str ("locale " ^ cond_extern sg name ^ " =") ::
        (if null imports then [] else
-       (flat (separate [Pretty.str "+", Pretty.brk 1] (map (single o Pretty.str) imports)) @
-         [Pretty.str "+"])));
+       (Pretty.str " " :: flat (separate [Pretty.str " +", Pretty.brk 1]
+           (map (single o Pretty.str o cond_extern sg) imports)) @ [Pretty.str " +"])));
   in Pretty.block (Pretty.fbreaks (prt_header :: map prt_elem elements)) end;
 
 val print_locale = Pretty.writeln oo pretty_locale;
 
 

 fun closeup ctxt (Assumes asms) = Assumes (asms |> map (fn (a, propps) =>
       (a, propps |> map (fn (t, (ps1, ps2)) =>
         let val close = close_frees_wrt ctxt t in (close t, (map close ps1, map close ps2)) end))))
   | closeup ctxt (Defines defs) = Defines (defs |> map (fn (a, (t, ps)) =>
       let
-        val t' = ProofContext.cert_def ctxt t;
+        val (_, t') = ProofContext.cert_def ctxt t;
         val close = close_frees_wrt ctxt t';
       in (a, (close t', map close ps)) end))
   | closeup ctxt elem = elem;
 
 

 (** store results **)
 
 fun store_thm name ((a, th), atts) thy =
   let
     val {imports, elements, closed} = the_locale thy name;
-    val _ = conditional closed
-      (fn () => error ("Cannot store results in closed locale: " ^ quote name));
     val note = Notes [((a, atts), [([Thm.name_thm (a, th)], [])])];
   in
+    conditional closed (fn () => error ("Cannot store results in closed locale: " ^ quote name));
     activate (ProofContext.init thy |> activate_locale_i name, note);    (*test attribute*)
     thy |> put_locale name (make_locale imports (elements @ [note]) closed)
   end;