# HG changeset patch # User haftmann # Date 1388355671 -3600 # Node ID b370e1622e411ebaade9febaeade5f025c6c782b # Parent c55c5dacd6a1af601621636538e77d3b7ce580df tuned whitespace diff -r c55c5dacd6a1 -r b370e1622e41 src/Pure/Isar/expression.ML --- 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