# HG changeset patch
# User haftmann
# Date 1231311805 -3600
# Node ID 2821c2c5270d3847b49c18e96be72a75fd3124d8
# Parent  ff4ba1ed4527c0b361c8add03433457a79d272da
proper local_theory after Class.class

diff -r ff4ba1ed4527 -r 2821c2c5270d src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Jan 06 09:18:02 2009 -0800
+++ b/src/Pure/Isar/class.ML	Wed Jan 07 08:03:25 2009 +0100
@@ -11,9 +11,9 @@
       ML is artificial*)
 
   val class: bstring -> class list -> Element.context_i list
-    -> theory -> string * Proof.context
+    -> theory -> string * local_theory
   val class_cmd: bstring -> xstring list -> Element.context list
-    -> theory -> string * Proof.context
+    -> theory -> string * local_theory
   val prove_subclass: tactic -> class -> local_theory -> local_theory
   val subclass: class -> local_theory -> Proof.state
   val subclass_cmd: xstring -> local_theory -> Proof.state
@@ -208,7 +208,7 @@
         register class sups params base_sort inst
           morphism axiom assm_intro of_class
     #> fold (note_assm_intro class) (the_list assm_intro))))))
-    |> init class
+    |> TheoryTarget.init (SOME class)
     |> pair class
   end;
 
diff -r ff4ba1ed4527 -r 2821c2c5270d src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jan 06 09:18:02 2009 -0800
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jan 07 08:03:25 2009 +0100
@@ -470,7 +470,7 @@
    (P.name -- (P.$$$ "=" |-- class_val) -- P.opt_begin
     >> (fn ((name, (supclasses, elems)), begin) =>
         (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
-          (Class.class_cmd name supclasses elems #-> TheoryTarget.begin)));
+          (Class.class_cmd name supclasses elems #> snd)));
 
 val _ =
   OuterSyntax.local_theory_to_proof "subclass" "prove a subclass relation" K.thy_goal