src/Pure/Isar/expression.ML
changeset 38756 d07959fabde6
parent 38389 d7d915bae307
child 38757 2b3e054ae6fc
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Aug 26 12:06:00 2010 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Aug 26 13:09:12 2010 +0200
     1.3 @@ -824,7 +824,7 @@
     1.4      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     1.5      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
     1.6  
     1.7 -    fun after_qed witss eqns = (ProofContext.theory o Context.theory_map)
     1.8 +    fun after_qed witss eqns = (ProofContext.background_theory o Context.theory_map)
     1.9        (note_eqns_register deps witss attrss eqns export export');
    1.10  
    1.11    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
    1.12 @@ -872,7 +872,7 @@
    1.13      val target = intern thy raw_target;
    1.14      val target_ctxt = Named_Target.init target thy;
    1.15      val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
    1.16 -    fun after_qed witss = ProofContext.theory
    1.17 +    fun after_qed witss = ProofContext.background_theory
    1.18        (fold (fn ((dep, morph), wits) => Locale.add_dependency
    1.19          target (dep, morph $> Element.satisfy_morphism wits) export) (deps ~~ witss));
    1.20    in Element.witness_proof after_qed propss goal_ctxt end;