merged

--- a/src/Pure/Isar/class.ML	Tue Jan 06 22:08:42 2009 +0100
+++ b/src/Pure/Isar/class.ML	Wed Jan 07 08:04:12 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;
 

--- a/src/Pure/Isar/isar_syn.ML	Tue Jan 06 22:08:42 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jan 07 08:04:12 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