src/Pure/Isar/expression.ML
changeset 54875 b370e1622e41
parent 54865 82bfac35f16f
child 54876 8fab871a2a6f
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Dec 28 21:06:26 2013 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Dec 29 23:21:11 2013 +0100
     1.3 @@ -851,7 +851,7 @@
     1.4      val dep_morphs = map2 (fn (dep, morph) => fn wits =>
     1.5        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
     1.6      fun activate' dep_morph ctxt = activate dep_morph
     1.7 -        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
     1.8 +      (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
     1.9    in
    1.10      ctxt'
    1.11      |> fold activate' dep_morphs