Intro_locales_tac knows about defines elements; more robust export morphism.

--- a/src/Pure/Isar/expression.ML	Fri Dec 19 11:57:21 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Dec 19 14:31:07 2008 +0100
@@ -459,7 +459,7 @@
 
     val export = Variable.export_morphism goal_ctxt context;
     val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
-    val exp_term = Drule.term_rule thy (singleton exp_fact);
+    val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
     val exp_typ = Logic.type_map exp_term;
     val export' =
       Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
@@ -688,7 +688,8 @@
 
 fun defines_to_notes thy (Defines defs) =
       Notes (Thm.definitionK, map (fn (a, (def, _)) =>
-        (a, [([Assumption.assume (cterm_of thy def)], [])])) defs)
+        (a, [([Assumption.assume (cterm_of thy def)],
+          [(Attrib.internal o K) NewLocale.witness_attrib])])) defs)
   | defines_to_notes _ e = e;
 
 fun gen_add_locale prep_decl