1.1 --- a/src/Pure/Isar/class.ML	Thu Aug 26 12:06:00 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Aug 26 13:09:12 2010 +0200
     1.3 @@ -368,7 +368,7 @@
     1.4  fun gen_classrel mk_prop classrel thy =
     1.5    let
     1.6      fun after_qed results =
     1.7 -      ProofContext.theory ((fold o fold) AxClass.add_classrel results);
     1.8 +      ProofContext.background_theory ((fold o fold) AxClass.add_classrel results);
     1.9    in
    1.10      thy
    1.11      |> ProofContext.init_global
    1.12 @@ -608,7 +608,7 @@
    1.13      val (tycos, vs, sort) = read_multi_arity thy raw_arities;
    1.14      val sorts = map snd vs;
    1.15      val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
    1.16 -    fun after_qed results = ProofContext.theory
    1.17 +    fun after_qed results = ProofContext.background_theory
    1.18        ((fold o fold) AxClass.add_arity results);
    1.19    in
    1.20      thy