src/Pure/theory.ML

   val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
   val add_defs: bool -> bool -> (bstring * string) list -> theory -> theory
   val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory
   val add_finals: bool -> string list -> theory -> theory
   val add_finals_i: bool -> term list -> theory -> theory
-  val specify_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
+  val specify_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory
 end
 
 structure Theory: THEORY =
 struct
 

 (* check_def *)
 
 fun check_def thy unchecked overloaded (bname, tm) defs =
   let
     val ctxt = ProofContext.init thy;
-    val name = Sign.full_name thy bname;
+    val name = Sign.full_bname thy bname;
     val (lhs_const, rhs) = Sign.cert_def ctxt tm;
     val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
     val _ = check_overloading thy overloaded lhs_const;
   in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block