src/Pure/Isar/expression.ML

--- a/src/Pure/Isar/expression.ML	Sun Sep 27 11:50:27 2009 +0200
+++ b/src/Pure/Isar/expression.ML	Tue Sep 29 22:15:54 2009 +0200
@@ -818,8 +818,9 @@
 
     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)));
+        fn thy => Locale.add_registration (dep, morph $> Element.satisfy_morphism
+            (map (Element.morph_witness export') wits))
+          (Element.eq_morphism thy eqns, true) export thy) (deps ~~ witss)));
 
   in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;