src/Pure/Isar/expression.ML

       |> note Thm.lemmaK facts
       |-> meta_rewrite;
     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
   end;