src/Pure/Isar/expression.ML
changeset 38107 3a46cebd7983
parent 37313 715d25555ca6
child 38108 b4115423c049
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Jul 30 15:03:42 2010 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Jul 31 21:14:20 2010 +0200
     1.3 @@ -821,10 +821,11 @@
     1.4  
     1.5      fun after_qed witss eqns = ProofContext.theory (note_eqns eqns
     1.6        #-> (fn eqns => fold (fn ((dep, morph), wits) =>
     1.7 -        fn thy => Locale.add_registration (dep, morph $> Element.satisfy_morphism
     1.8 -            (map (Element.morph_witness export') wits))
     1.9 -          (Element.eq_morphism thy eqns |> Option.map (rpair true))
    1.10 -          export thy) (deps ~~ witss)));
    1.11 +        fn thy => Context.theory_map
    1.12 +          (Locale.add_registration (dep, morph $> Element.satisfy_morphism
    1.13 +              (map (Element.morph_witness export') wits))
    1.14 +            (Element.eq_morphism thy eqns |> Option.map (rpair true))
    1.15 +            export) thy) (deps ~~ witss)));
    1.16  
    1.17    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
    1.18