# HG changeset patch
# User haftmann
# Date 1194351173 -3600
# Node ID aa750e3a581c339628d837b18ffc4aba59607a91
# Parent  2b928fb92f534b06749b6f5138ebd35b08f5677f
Class.init now similiar to Locale.init

diff -r 2b928fb92f53 -r aa750e3a581c src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Nov 06 13:12:52 2007 +0100
+++ b/src/Pure/Isar/class.ML	Tue Nov 06 13:12:53 2007 +0100
@@ -18,7 +18,7 @@
     -> xstring list -> theory -> string * Proof.context
   val is_class: theory -> class -> bool
   val these_params: theory -> sort -> (string * (string * typ)) list
-  val init: class -> Proof.context -> Proof.context
+  val init: class -> theory -> Proof.context
   val add_logical_const: string -> Markup.property list
     -> (string * mixfix) * term -> theory -> theory
   val add_syntactic_const: string -> Syntax.mode -> Markup.property list
@@ -716,12 +716,10 @@
       Syntax.add_term_check 0 "class" sort_term_check
       #> Syntax.add_term_uncheck 0 "class" sort_term_uncheck)
 
-fun init class ctxt =
-  let
-    val thy = ProofContext.theory_of ctxt;
-  in
-    init_ctxt thy [class] ((#base_sort o the_class_data thy) class) ctxt
-  end;
+fun init class thy =
+  thy
+  |> Locale.init class
+  |> init_ctxt thy [class] ((#base_sort o the_class_data thy) class);
 
 
 (* class definition *)
@@ -827,8 +825,9 @@
     thy
     |> Locale.add_locale_i (SOME "") bname mergeexpr elems
     |> snd
-    |> ProofContext.theory (`extract_params
-      #-> (fn (all_params, params) =>
+    |> ProofContext.theory_of
+    |> `extract_params
+    |-> (fn (all_params, params) =>
         define_class_params (bname, supsort) params
           (extract_assumes params) other_consts
       #-> (fn (_, (consts, axioms)) =>
@@ -842,7 +841,7 @@
             mk_inst class (map snd supconsts @ consts),
               calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro))
       #> class_interpretation class axioms []
-      )))))
+      ))))
     |> init class
     |> pair class
   end;
diff -r 2b928fb92f53 -r aa750e3a581c src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Nov 06 13:12:52 2007 +0100
+++ b/src/Pure/Isar/theory_target.ML	Tue Nov 06 13:12:53 2007 +0100
@@ -305,8 +305,8 @@
   | init_target thy (SOME target) = make_target target true (Class.is_class thy target);
 
 fun init_ctxt (Target {target, is_locale, is_class}) =
-  (if is_locale then Locale.init target else ProofContext.init) #>
-  is_class ? Class.init target;
+  if is_locale then if is_class then Class.init target
+    else Locale.init target else ProofContext.init;
 
 fun init_lthy (ta as Target {target, ...}) =
   Data.put ta #>