1.1 --- a/src/HOLCF/Tools/pcpodef.ML	Thu Aug 26 12:06:00 2010 +0200
     1.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Thu Aug 26 13:09:12 2010 +0200
     1.3 @@ -326,7 +326,7 @@
     1.4      val args = map (apsnd (prep_constraint ctxt)) raw_args;
     1.5      val (goal1, goal2, make_result) =
     1.6        prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
     1.7 -    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
     1.8 +    fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
     1.9        | after_qed _ = raise Fail "cpodef_proof";
    1.10    in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
    1.11  
    1.12 @@ -337,7 +337,7 @@
    1.13      val args = map (apsnd (prep_constraint ctxt)) raw_args;
    1.14      val (goal1, goal2, make_result) =
    1.15        prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
    1.16 -    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
    1.17 +    fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
    1.18        | after_qed _ = raise Fail "pcpodef_proof";
    1.19    in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
    1.20