# HG changeset patch # User wenzelm # Date 1160600123 -7200 # Node ID 808ae04981beb5a381700d6b1be32ca9beeb604a # Parent de13e2a23c8e678ad2d290494aa47865d0f12cef tuned Toplevel.begin_local_theory; diff -r de13e2a23c8e -r 808ae04981be src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Wed Oct 11 22:55:22 2006 +0200 +++ b/src/Pure/Tools/class_package.ML Wed Oct 11 22:55:23 2006 +0200 @@ -595,7 +595,7 @@ || class_bodyP >> pair []) -- P.opt_begin >> (fn ((bname, (supclasses, elems)), begin) => - Toplevel.begin_local_theory begin (class bname supclasses elems))); + Toplevel.begin_local_theory begin (class bname supclasses elems #-> TheoryTarget.begin))); val instanceP = OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((