1.1 --- a/src/Pure/Isar/constdefs.ML	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/Pure/Isar/constdefs.ML	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Pure/Isar/constdefs.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
     1.7  
     1.8  Old-style constant definitions, with type-inference and optional
     1.9 @@ -9,12 +8,12 @@
    1.10  
    1.11  signature CONSTDEFS =
    1.12  sig
    1.13 -  val add_constdefs: (Name.binding * string option) list *
    1.14 -    ((Name.binding * string option * mixfix) option *
    1.15 +  val add_constdefs: (Binding.T * string option) list *
    1.16 +    ((Binding.T * string option * mixfix) option *
    1.17        (Attrib.binding * string)) list -> theory -> theory
    1.18 -  val add_constdefs_i: (Name.binding * typ option) list *
    1.19 -    ((Name.binding * typ option * mixfix) option *
    1.20 -      ((Name.binding * attribute list) * term)) list -> theory -> theory
    1.21 +  val add_constdefs_i: (Binding.T * typ option) list *
    1.22 +    ((Binding.T * typ option * mixfix) option *
    1.23 +      ((Binding.T * attribute list) * term)) list -> theory -> theory
    1.24  end;
    1.25  
    1.26  structure Constdefs: CONSTDEFS =
    1.27 @@ -46,7 +45,7 @@
    1.28              err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
    1.29            else ());
    1.30  
    1.31 -    val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name thy c, T))] prop;
    1.32 +    val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
    1.33      val name = Thm.def_name_optional c (Name.name_of raw_name);
    1.34      val atts = map (prep_att thy) raw_atts;
    1.35