--- a/src/HOL/Nominal/nominal_induct.ML Wed Dec 03 21:00:39 2008 -0800
+++ b/src/HOL/Nominal/nominal_induct.ML Thu Dec 04 14:43:33 2008 +0100
@@ -6,7 +6,7 @@
structure NominalInduct:
sig
- val nominal_induct_tac: Proof.context -> (Name.binding option * term) option list list ->
+ val nominal_induct_tac: Proof.context -> (Binding.T option * term) option list list ->
(string * typ) list -> (string * typ) list list -> thm list ->
thm list -> int -> RuleCases.cases_tactic
val nominal_induct_method: Method.src -> Proof.context -> Method.method