--- a/src/Pure/Isar/class_declaration.ML Wed Dec 25 22:35:28 2013 +0100
+++ b/src/Pure/Isar/class_declaration.ML Wed Dec 25 22:35:29 2013 +0100
@@ -355,9 +355,7 @@
val some_prop = try the_single props;
val some_dep_morph = try the_single (map snd deps);
fun after_qed some_wit =
- Proof_Context.background_theory (Class.register_subclass (sub, sup)
- some_dep_morph some_wit export)
- #> Proof_Context.theory_of #> Named_Target.init before_exit sub;
+ Class.register_subclass (sub, sup) some_dep_morph some_wit export;
in do_proof after_qed some_prop goal_ctxt end;
fun user_proof after_qed some_prop =