--- a/src/Pure/Isar/expression.ML Sat Dec 28 21:06:26 2013 +0100
+++ b/src/Pure/Isar/expression.ML Sun Dec 29 23:21:11 2013 +0100
@@ -851,7 +851,7 @@
val dep_morphs = map2 (fn (dep, morph) => fn wits =>
(dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
fun activate' dep_morph ctxt = activate dep_morph
- (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
+ (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
in
ctxt'
|> fold activate' dep_morphs