--- a/src/Pure/Isar/expression.ML Fri Jul 30 15:03:42 2010 +0200
+++ b/src/Pure/Isar/expression.ML Sat Jul 31 21:14:20 2010 +0200
@@ -821,10 +821,11 @@
fun after_qed witss eqns = ProofContext.theory (note_eqns eqns
#-> (fn eqns => fold (fn ((dep, morph), wits) =>
- fn thy => Locale.add_registration (dep, morph $> Element.satisfy_morphism
- (map (Element.morph_witness export') wits))
- (Element.eq_morphism thy eqns |> Option.map (rpair true))
- export thy) (deps ~~ witss)));
+ fn thy => Context.theory_map
+ (Locale.add_registration (dep, morph $> Element.satisfy_morphism
+ (map (Element.morph_witness export') wits))
+ (Element.eq_morphism thy eqns |> Option.map (rpair true))
+ export) thy) (deps ~~ witss)));
in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;