src/ZF/Tools/induct_tacs.ML
changeset 15462 b4208fbf9439
parent 14153 76a6ba67bd15
child 15531 08c8dad8e399
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Mon Jan 24 18:12:22 2005 +0100
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Mon Jan 24 18:15:19 2005 +0100
     1.3 @@ -13,8 +13,8 @@
     1.4    val induct_tac: string -> int -> tactic
     1.5    val exhaust_tac: string -> int -> tactic
     1.6    val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
     1.7 -  val rep_datatype: xstring * Args.src list -> xstring * Args.src list ->
     1.8 -    (xstring * Args.src list) list -> (xstring * Args.src list) list -> theory -> theory
     1.9 +  val rep_datatype: thmref * Args.src list -> thmref * Args.src list ->
    1.10 +    (thmref * Args.src list) list -> (thmref * Args.src list) list -> theory -> theory
    1.11    val setup: (theory -> theory) list
    1.12  end;
    1.13  
    1.14 @@ -115,11 +115,8 @@
    1.15          (case prems_of rule of
    1.16               [] => error "induction is not available for this datatype"
    1.17             | major::_ => FOLogic.dest_Trueprop major)
    1.18 -    val ind_vname = Syntax.string_of_vname ixn
    1.19 -    val vname' = (*delete leading question mark*)
    1.20 -        String.substring (ind_vname, 1, size ind_vname-1)
    1.21    in
    1.22 -    eres_inst_tac [(vname',var)] rule i state
    1.23 +    Tactic.eres_inst_tac' [(ixn, var)] rule i state
    1.24    end
    1.25    handle Find_tname msg =>
    1.26              if exh then (*try boolean case analysis instead*)