src/Pure/Isar/expression.ML

       in
         thy
         |> PureThy.note_thmss Thm.lemmaK eqn_attrss
         |-> (fn facts => `(fn thy => meta_rewrite thy facts))
       end;
-
+(*
     fun after_qed witss eqns = ProofContext.theory (note_eqns eqns
       #-> (fn eqns => fold (fn ((dep, morph), wits) =>
         Locale.add_registration_eqs (dep, morph $> Element.satisfy_morphism
           (map (Element.morph_witness export') wits)) eqns export) (deps ~~ witss)));
+*)
+    fun after_qed witss eqns = ProofContext.theory (note_eqns eqns
+      #-> (fn eqns => fold (fn ((dep, morph), wits) =>
+        Locale.add_registration (dep, morph $> Element.satisfy_morphism
+          (map (Element.morph_witness export') wits)) export
+         #> not (null eqns) ? (fn thy => Locale.amend_registration (Element.eq_morphism thy eqns, true) (dep, morph) thy)) (deps ~~ witss)));
 
   in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
 
 in