1.1 --- a/src/Tools/induct.ML	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/Tools/induct.ML	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Tools/induct.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Markus Wenzel, TU Muenchen
     1.7  
     1.8  Proof by cases, induction, and coinduction.
     1.9 @@ -51,7 +50,7 @@
    1.10    val setN: string
    1.11    (*proof methods*)
    1.12    val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
    1.13 -  val add_defs: (Name.binding option * term) option list -> Proof.context ->
    1.14 +  val add_defs: (Binding.T option * term) option list -> Proof.context ->
    1.15      (term option list * thm list) * Proof.context
    1.16    val atomize_term: theory -> term -> term
    1.17    val atomize_tac: int -> tactic
    1.18 @@ -63,7 +62,7 @@
    1.19    val cases_tac: Proof.context -> term option list list -> thm option ->
    1.20      thm list -> int -> cases_tactic
    1.21    val get_inductT: Proof.context -> term option list list -> thm list list
    1.22 -  val induct_tac: Proof.context -> (Name.binding option * term) option list list ->
    1.23 +  val induct_tac: Proof.context -> (Binding.T option * term) option list list ->
    1.24      (string * typ) list list -> term option list -> thm list option ->
    1.25      thm list -> int -> cases_tactic
    1.26    val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
    1.27 @@ -553,7 +552,7 @@
    1.28    let
    1.29      fun add (SOME (SOME x, t)) ctxt =
    1.30            let val ([(lhs, (_, th))], ctxt') =
    1.31 -            LocalDefs.add_defs [((x, NoSyn), ((Name.no_binding, []), t))] ctxt
    1.32 +            LocalDefs.add_defs [((x, NoSyn), ((Binding.empty, []), t))] ctxt
    1.33            in ((SOME lhs, [th]), ctxt') end
    1.34        | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
    1.35        | add NONE ctxt = ((NONE, []), ctxt);