--- a/src/Pure/Isar/class_declaration.ML Thu Aug 26 12:06:00 2010 +0200
+++ b/src/Pure/Isar/class_declaration.ML Thu Aug 26 13:09:12 2010 +0200
@@ -330,7 +330,7 @@
val some_prop = try the_single props;
val some_dep_morph = try the_single (map snd deps);
fun after_qed some_wit =
- ProofContext.theory (Class.register_subclass (sub, sup)
+ ProofContext.background_theory (Class.register_subclass (sub, sup)
some_dep_morph some_wit export)
#> ProofContext.theory_of #> Named_Target.init sub;
in do_proof after_qed some_prop goal_ctxt end;