# HG changeset patch
# User wenzelm
# Date 1160519259 -7200
# Node ID 77b59c3a2418c1f463a370ae6ef40f2fffee3500
# Parent  a7fd8f05a2bee7842ef91a9dd371945ca3c496cf
class(_i): mimic Locale.add_locale(_i);
'class': begin_local_theory;

diff -r a7fd8f05a2be -r 77b59c3a2418 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Wed Oct 11 00:27:38 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Wed Oct 11 00:27:39 2006 +0200
@@ -7,10 +7,10 @@
 
 signature CLASS_PACKAGE =
 sig
-  val class: bstring -> class list -> Element.context Locale.element list -> theory
-    -> Proof.context * theory
-  val class_i: bstring -> class list -> Element.context_i Locale.element list -> theory
-    -> Proof.context * theory
+  val class: bstring -> class list -> Element.context Locale.element list -> theory ->
+    string * Proof.context
+  val class_i: bstring -> class list -> Element.context_i Locale.element list -> theory ->
+    string * Proof.context
   val instance_arity: ((bstring * string list) * string) list
     -> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list
     -> theory -> Proof.state
@@ -320,8 +320,8 @@
   in
     thy
     |> add_locale bname expr elems
-    |-> (fn (name_locale, ctxt) =>
-          `(fn thy => extract_tyvar_consts thy name_locale)
+    |-> (fn name_locale => ProofContext.theory
+          (`(fn thy => extract_tyvar_consts thy name_locale)
     #-> (fn (v, (raw_cs_sup, raw_cs_this)) =>
           add_consts v raw_cs_sup raw_cs_this
     #-> (fn mapp_this =>
@@ -336,8 +336,7 @@
     #> prove_interpretation_i (bname, [])
           (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this)))
           ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
-    #> pair ctxt
-    )))))
+    ))))) #> pair name_locale)
   end;
 
 in
@@ -593,9 +592,10 @@
     -- (
       class_subP --| P.$$$ "+" -- class_bodyP
       || class_subP >> rpair []
-      || class_bodyP >> pair []
-    ) >> (Toplevel.theory_context
-          o (fn (bname, (supclasses, elems)) => class bname supclasses elems)));
+      || class_bodyP >> pair [])
+    -- P.opt_begin
+    >> (fn ((bname, (supclasses, elems)), begin) =>
+        Toplevel.begin_local_theory begin (class bname supclasses elems)));
 
 val instanceP =
   OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((