src/Pure/Isar/expression.ML
changeset 46856 28909eecdf5b
parent 45589 bb944d58ac19
child 46858 05f30c796f95
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Mar 10 16:49:34 2012 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Mar 10 17:07:10 2012 +0100
     1.3 @@ -899,8 +899,7 @@
     1.4      |> Proof_Context.background_theory (fold (fn ((dep, morph), wits) =>
     1.5        fn thy =>
     1.6          Locale.add_dependency target
     1.7 -          (dep, morph $> Element.satisfy_morphism
     1.8 -            (map (Element.transform_witness export') wits))
     1.9 +          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
    1.10            (Element.eq_morphism thy eqns' |> Option.map (rpair true))
    1.11            export thy) (deps ~~ witss))
    1.12    end;