src/Pure/Isar/class_declaration.ML
changeset 54866 7b9a67cbd48f
parent 54742 7a86358a3c0b
child 54882 61276a7fc369
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Wed Dec 25 22:35:28 2013 +0100
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Wed Dec 25 22:35:29 2013 +0100
     1.3 @@ -355,9 +355,7 @@
     1.4      val some_prop = try the_single props;
     1.5      val some_dep_morph = try the_single (map snd deps);
     1.6      fun after_qed some_wit =
     1.7 -      Proof_Context.background_theory (Class.register_subclass (sub, sup)
     1.8 -        some_dep_morph some_wit export)
     1.9 -      #> Proof_Context.theory_of #> Named_Target.init before_exit sub;
    1.10 +      Class.register_subclass (sub, sup) some_dep_morph some_wit export;
    1.11    in do_proof after_qed some_prop goal_ctxt end;
    1.12  
    1.13  fun user_proof after_qed some_prop =