1.1 --- a/src/Pure/Isar/named_target.ML	Wed Aug 11 15:45:15 2010 +0200
     1.2 +++ b/src/Pure/Isar/named_target.ML	Wed Aug 11 16:02:03 2010 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  fun named_target _ NONE = global_target
     1.5    | named_target thy (SOME locale) =
     1.6        if Locale.defined thy locale
     1.7 -      then Target {target = locale, is_locale = true, is_class = Class_Target.is_class thy locale}
     1.8 +      then Target {target = locale, is_locale = true, is_class = Class.is_class thy locale}
     1.9        else error ("No such locale: " ^ quote locale);
    1.10  
    1.11  structure Data = Proof_Data
    1.12 @@ -69,7 +69,7 @@
    1.13      val is_canonical_class = is_class andalso
    1.14        (Binding.eq_name (b, b')
    1.15          andalso not (null prefix')
    1.16 -        andalso List.last prefix' = (Class_Target.class_prefix target, false)
    1.17 +        andalso List.last prefix' = (Class.class_prefix target, false)
    1.18        orelse same_shape);
    1.19    in
    1.20      not is_canonical_class ?
    1.21 @@ -88,7 +88,7 @@
    1.22  
    1.23  fun class_target (Target {target, ...}) f =
    1.24    Local_Theory.raw_theory f #>
    1.25 -  Local_Theory.target (Class_Target.refresh_syntax target);
    1.26 +  Local_Theory.target (Class.refresh_syntax target);
    1.27  
    1.28  
    1.29  (* define *)
    1.30 @@ -102,7 +102,7 @@
    1.31      (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
    1.32    Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    1.33    #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
    1.34 -    #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs)))
    1.35 +    #> class_target ta (Class.declare target ((b, mx), (type_params, lhs)))
    1.36      #> pair (lhs, def))
    1.37  
    1.38  fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =
    1.39 @@ -141,7 +141,7 @@
    1.40    if is_locale
    1.41      then lthy
    1.42        |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
    1.43 -      |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t'))
    1.44 +      |> is_class ? class_target ta (Class.abbrev target prmode ((b, mx), t'))
    1.45      else lthy
    1.46        |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
    1.47  
    1.48 @@ -181,7 +181,7 @@
    1.49  fun init_context (Target {target, is_locale, is_class}) =
    1.50    if not is_locale then ProofContext.init_global
    1.51    else if not is_class then Locale.init target
    1.52 -  else Class_Target.init target;
    1.53 +  else Class.init target;
    1.54  
    1.55  fun init_target (ta as Target {target, ...}) thy =
    1.56    thy