--- a/src/HOL/Nominal/nominal_primrec.ML Wed Dec 03 21:00:39 2008 -0800
+++ b/src/HOL/Nominal/nominal_primrec.ML Thu Dec 04 14:43:33 2008 +0100
@@ -9,13 +9,13 @@
signature NOMINAL_PRIMREC =
sig
val add_primrec: string -> string list option -> string option ->
- ((Name.binding * string) * Attrib.src list) list -> theory -> Proof.state
+ ((Binding.T * string) * Attrib.src list) list -> theory -> Proof.state
val add_primrec_unchecked: string -> string list option -> string option ->
- ((Name.binding * string) * Attrib.src list) list -> theory -> Proof.state
+ ((Binding.T * string) * Attrib.src list) list -> theory -> Proof.state
val add_primrec_i: string -> term list option -> term option ->
- ((Name.binding * term) * attribute list) list -> theory -> Proof.state
+ ((Binding.T * term) * attribute list) list -> theory -> Proof.state
val add_primrec_unchecked_i: string -> term list option -> term option ->
- ((Name.binding * term) * attribute list) list -> theory -> Proof.state
+ ((Binding.T * term) * attribute list) list -> theory -> Proof.state
end;
structure NominalPrimrec : NOMINAL_PRIMREC =