src/Tools/induct.ML
changeset 28083 103d9282a946
parent 27865 27a8ad9612a3
child 28375 c879d88d038a
     1.1 --- a/src/Tools/induct.ML	Tue Sep 02 14:10:32 2008 +0200
     1.2 +++ b/src/Tools/induct.ML	Tue Sep 02 14:10:45 2008 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4    val setN: string
     1.5    (*proof methods*)
     1.6    val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
     1.7 -  val add_defs: (string option * term) option list -> Proof.context ->
     1.8 +  val add_defs: (Name.binding option * term) option list -> Proof.context ->
     1.9      (term option list * thm list) * Proof.context
    1.10    val atomize_term: theory -> term -> term
    1.11    val atomize_tac: int -> tactic
    1.12 @@ -63,7 +63,7 @@
    1.13    val cases_tac: Proof.context -> term option list list -> thm option ->
    1.14      thm list -> int -> cases_tactic
    1.15    val get_inductT: Proof.context -> term option list list -> thm list list
    1.16 -  val induct_tac: Proof.context -> (string option * term) option list list ->
    1.17 +  val induct_tac: Proof.context -> (Name.binding option * term) option list list ->
    1.18      (string * typ) list list -> term option list -> thm list option ->
    1.19      thm list -> int -> cases_tactic
    1.20    val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
    1.21 @@ -552,7 +552,8 @@
    1.22  fun add_defs def_insts =
    1.23    let
    1.24      fun add (SOME (SOME x, t)) ctxt =
    1.25 -          let val ([(lhs, (_, th))], ctxt') = LocalDefs.add_defs [((x, NoSyn), (("", []), t))] ctxt
    1.26 +          let val ([(lhs, (_, th))], ctxt') =
    1.27 +            LocalDefs.add_defs [((x, NoSyn), ((Name.no_binding, []), t))] ctxt
    1.28            in ((SOME lhs, [th]), ctxt') end
    1.29        | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
    1.30        | add NONE ctxt = ((NONE, []), ctxt);
    1.31 @@ -716,7 +717,7 @@
    1.32  val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
    1.33  
    1.34  val def_inst =
    1.35 -  ((Scan.lift (Args.name --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
    1.36 +  ((Scan.lift (Args.binding --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
    1.37        -- Args.term) >> SOME ||
    1.38      inst >> Option.map (pair NONE);
    1.39