# HG changeset patch
# User haftmann
# Date 1205565077 -3600
# Node ID 3386bb568550110d3c051a72c3b987ee12eddfe1
# Parent  014d93dc21996407c105a705f75c02870c06e9cd
explicit re-init

diff -r 014d93dc2199 -r 3386bb568550 src/Pure/Isar/subclass.ML
--- a/src/Pure/Isar/subclass.ML	Sat Mar 15 08:11:16 2008 +0100
+++ b/src/Pure/Isar/subclass.ML	Sat Mar 15 08:11:17 2008 +0100
@@ -37,7 +37,7 @@
       |> ObjectLogic.ensure_propT thy;
     fun after_qed thm =
       LocalTheory.theory (Class.prove_subclass (sub, sup) thm)
-      #> LocalTheory.reinit;
+      #> (TheoryTarget.init (SOME sub) o ProofContext.theory_of);
   in
     do_proof after_qed sublocale_prop lthy
   end;