src/Pure/Isar/class.ML

   val declare: class -> Properties.T
     -> (string * mixfix) * term -> theory -> theory
   val abbrev: class -> Syntax.mode -> Properties.T
     -> (string * mixfix) * term -> theory -> theory
   val note: class -> string
-    -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list
+    -> (Attrib.binding * (thm list * Attrib.src list) list) list
     -> theory -> (bstring * thm list) list * theory
   val declaration: class -> declaration -> theory -> theory
   val refresh_syntax: class -> Proof.context -> Proof.context
 
   val intro_classes_tac: thm list -> tactic

   val pretty_instantiation: local_theory -> Pretty.T
   val type_name: string -> string
 
   (*old axclass layer*)
   val axclass_cmd: bstring * xstring list
-    -> ((Name.binding * Attrib.src list) * string list) list
+    -> (Attrib.binding * string list) list
     -> theory -> class * theory
   val classrel_cmd: xstring * xstring -> theory -> Proof.state
 
   (*old instance layer*)
   val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state

     val prfx = class_prefix class;
   in
     thy
     |> fold2 add_constraint (map snd consts) no_constraints
     |> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
-          (inst, map (fn def => ((Name.no_binding, []), def)) defs)
+          (inst, map (fn def => (Attrib.no_binding, def)) defs)
     |> fold2 add_constraint (map snd consts) constraints
   end;
 
 fun prove_subclass (sub, sup) some_thm thy =
   let