1.1 --- a/src/Pure/Isar/constdefs.ML	Wed Jan 21 16:47:03 2009 +0100
     1.2 +++ b/src/Pure/Isar/constdefs.ML	Wed Jan 21 16:47:04 2009 +0100
     1.3 @@ -8,12 +8,12 @@
     1.4  
     1.5  signature CONSTDEFS =
     1.6  sig
     1.7 -  val add_constdefs: (Binding.T * string option) list *
     1.8 -    ((Binding.T * string option * mixfix) option *
     1.9 +  val add_constdefs: (binding * string option) list *
    1.10 +    ((binding * string option * mixfix) option *
    1.11        (Attrib.binding * string)) list -> theory -> theory
    1.12 -  val add_constdefs_i: (Binding.T * typ option) list *
    1.13 -    ((Binding.T * typ option * mixfix) option *
    1.14 -      ((Binding.T * attribute list) * term)) list -> theory -> theory
    1.15 +  val add_constdefs_i: (binding * typ option) list *
    1.16 +    ((binding * typ option * mixfix) option *
    1.17 +      ((binding * attribute list) * term)) list -> theory -> theory
    1.18  end;
    1.19  
    1.20  structure Constdefs: CONSTDEFS =
    1.21 @@ -52,7 +52,7 @@
    1.22      val thy' =
    1.23        thy
    1.24        |> Sign.add_consts_i [(c, T, mx)]
    1.25 -      |> PureThy.add_defs false [((name, def), atts)]
    1.26 +      |> PureThy.add_defs false [((Binding.name name, def), atts)]
    1.27        |-> (fn [thm] => Code.add_default_eqn thm);
    1.28    in ((c, T), thy') end;
    1.29