src/Pure/Isar/expression.ML
changeset 54875 b370e1622e41
parent 54865 82bfac35f16f
child 54876 8fab871a2a6f
equal deleted inserted replaced
54874:c55c5dacd6a1 54875:b370e1622e41
   849       |> note Thm.lemmaK facts
   849       |> note Thm.lemmaK facts
   850       |-> meta_rewrite;
   850       |-> meta_rewrite;
   851     val dep_morphs = map2 (fn (dep, morph) => fn wits =>
   851     val dep_morphs = map2 (fn (dep, morph) => fn wits =>
   852       (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
   852       (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
   853     fun activate' dep_morph ctxt = activate dep_morph
   853     fun activate' dep_morph ctxt = activate dep_morph
   854         (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
   854       (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
   855   in
   855   in
   856     ctxt'
   856     ctxt'
   857     |> fold activate' dep_morphs
   857     |> fold activate' dep_morphs
   858   end;
   858   end;
   859 
   859