src/Pure/Isar/expression.ML
changeset 32845 d2d0b9b1a69d
parent 32805 9b535493ac8d
child 32847 88b58880d52c
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Oct 01 07:40:25 2009 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Oct 01 20:37:33 2009 +0200
     1.3 @@ -820,7 +820,8 @@
     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 -          (Element.eq_morphism thy eqns, true) export thy) (deps ~~ witss)));
     1.8 +          (if null eqns then NONE else SOME (Element.eq_morphism thy eqns, true))
     1.9 +          export thy) (deps ~~ witss)));
    1.10  
    1.11    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
    1.12