tuned: less formal noise in Named_Target, more coherence in Class

--- a/src/Pure/Isar/class.ML	Thu Aug 19 18:44:26 2010 +0200
+++ b/src/Pure/Isar/class.ML	Fri Aug 20 08:52:01 2010 +0200
@@ -17,9 +17,8 @@
   val print_classes: theory -> unit
   val init: class -> theory -> Proof.context
   val begin: class list -> sort -> Proof.context -> Proof.context
-  val const: class -> (binding * mixfix) * (term list * term) -> theory -> theory
-  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
-  val refresh_syntax: class -> Proof.context -> Proof.context
+  val const: class -> (binding * mixfix) * (term list * term) -> local_theory -> local_theory
+  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
   val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
   val class_prefix: string -> string
   val register: class -> class list -> ((string * typ) * (string * typ)) list
@@ -286,12 +285,6 @@
     |> Overloading.set_primary_constraints
   end;
 
-fun refresh_syntax class ctxt =
-  let
-    val thy = ProofContext.theory_of ctxt;
-    val base_sort = base_sort thy class;
-  in synchronize_class_syntax [class] base_sort ctxt end;
-
 fun redeclare_operations thy sort =
   fold (redeclare_const thy o fst) (these_operations thy sort);
 
@@ -312,7 +305,15 @@
 
 val class_prefix = Logic.const_of_class o Long_Name.base_name;
 
-fun const class ((c, mx), (type_params, dict)) thy =
+fun target_extension f class lthy =
+  lthy
+  |> Local_Theory.raw_theory f
+  |> Local_Theory.target (synchronize_class_syntax [class]
+      (base_sort (ProofContext.theory_of lthy) class));
+
+local
+
+fun target_const class ((c, mx), (type_params, dict)) thy =
   let
     val morph = morphism thy class;
     val b = Morphism.binding morph c;
@@ -334,7 +335,7 @@
     |> Sign.add_const_constraint (c', SOME ty')
   end;
 
-fun abbrev class prmode ((c, mx), rhs) thy =
+fun target_abbrev class prmode ((c, mx), rhs) thy =
   let
     val morph = morphism thy class;
     val unchecks = these_unchecks thy [class];
@@ -352,6 +353,13 @@
     |> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE))
   end;
 
+in
+
+fun const class arg = target_extension (target_const class arg) class;
+fun abbrev class prmode arg = target_extension (target_abbrev class prmode arg) class;
+
+end;
+
 
 (* simple subclasses *)
 

--- a/src/Pure/Isar/named_target.ML	Thu Aug 19 18:44:26 2010 +0200
+++ b/src/Pure/Isar/named_target.ML	Fri Aug 20 08:52:01 2010 +0200
@@ -88,10 +88,6 @@
 fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
   locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg);
 
-fun class_target (Target {target, ...}) f =
-  Local_Theory.raw_theory f #>
-  Local_Theory.target (Class.refresh_syntax target);
-
 
 (* define *)
 
@@ -104,7 +100,7 @@
     (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
   Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
   #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
-    #> class_target ta (Class.const target ((b, mx), (type_params, lhs)))
+    #> Class.const target ((b, mx), (type_params, lhs))
     #> pair (lhs, def))
 
 fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =
@@ -143,7 +139,7 @@
   if is_locale
     then lthy
       |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
-      |> is_class ? class_target ta (Class.abbrev target prmode ((b, mx), t'))
+      |> is_class ? Class.abbrev target prmode ((b, mx), t')
     else lthy
       |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);