| changeset 29581 | b3b33e0298eb |
| parent 29276 | 94b1ffec9201 |
| child 30223 | 24d975352879 |
--- a/src/HOL/Nominal/nominal_primrec.ML Wed Jan 21 16:47:31 2009 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Wed Jan 21 16:47:32 2009 +0100 @@ -9,8 +9,8 @@ signature NOMINAL_PRIMREC = sig val add_primrec: term list option -> term option -> - (Binding.T * typ option * mixfix) list -> - (Binding.T * typ option * mixfix) list -> + (binding * typ option * mixfix) list -> + (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> local_theory -> Proof.state end;