src/Pure/Isar/expression.ML
changeset 36674 d95f39448121
parent 36610 bafd82950e24
child 37145 01aa36932739
     1.1 --- a/src/Pure/Isar/expression.ML	Wed May 05 09:24:41 2010 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed May 05 09:24:42 2010 +0200
     1.3 @@ -821,7 +821,7 @@
     1.4        #-> (fn eqns => fold (fn ((dep, morph), wits) =>
     1.5          fn thy => Locale.add_registration (dep, morph $> Element.satisfy_morphism
     1.6              (map (Element.morph_witness export') wits))
     1.7 -          (if null eqns then NONE else SOME (Element.eq_morphism thy eqns, true))
     1.8 +          (Element.eq_morphism thy eqns |> Option.map (rpair true))
     1.9            export thy) (deps ~~ witss)));
    1.10  
    1.11    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;