src/Pure/Isar/named_target.ML

--- a/src/Pure/Isar/named_target.ML	Wed Aug 11 15:45:15 2010 +0200
+++ b/src/Pure/Isar/named_target.ML	Wed Aug 11 16:02:03 2010 +0200
@@ -27,7 +27,7 @@
 fun named_target _ NONE = global_target
   | named_target thy (SOME locale) =
       if Locale.defined thy locale
-      then Target {target = locale, is_locale = true, is_class = Class_Target.is_class thy locale}
+      then Target {target = locale, is_locale = true, is_class = Class.is_class thy locale}
       else error ("No such locale: " ^ quote locale);
 
 structure Data = Proof_Data
@@ -69,7 +69,7 @@
     val is_canonical_class = is_class andalso
       (Binding.eq_name (b, b')
         andalso not (null prefix')
-        andalso List.last prefix' = (Class_Target.class_prefix target, false)
+        andalso List.last prefix' = (Class.class_prefix target, false)
       orelse same_shape);
   in
     not is_canonical_class ?
@@ -88,7 +88,7 @@
 
 fun class_target (Target {target, ...}) f =
   Local_Theory.raw_theory f #>
-  Local_Theory.target (Class_Target.refresh_syntax target);
+  Local_Theory.target (Class.refresh_syntax target);
 
 
 (* define *)
@@ -102,7 +102,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_Target.declare target ((b, mx), (type_params, lhs)))
+    #> class_target ta (Class.declare target ((b, mx), (type_params, lhs)))
     #> pair (lhs, def))
 
 fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =
@@ -141,7 +141,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_Target.abbrev target prmode ((b, mx), t'))
+      |> is_class ? class_target ta (Class.abbrev target prmode ((b, mx), t'))
     else lthy
       |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
 
@@ -181,7 +181,7 @@
 fun init_context (Target {target, is_locale, is_class}) =
   if not is_locale then ProofContext.init_global
   else if not is_class then Locale.init target
-  else Class_Target.init target;
+  else Class.init target;
 
 fun init_target (ta as Target {target, ...}) thy =
   thy