Eliminated hack for deleting leading question mark from induction
authorberghofe
Mon Jan 24 18:15:19 2005 +0100 (2005-01-24)
changeset 15462b4208fbf9439
parent 15461 d5d295a531b5
child 15463 95cb3eb74307
Eliminated hack for deleting leading question mark from induction
variable name.
src/Provers/ind.ML
src/ZF/Tools/induct_tacs.ML
     1.1 --- a/src/Provers/ind.ML	Mon Jan 24 18:12:22 2005 +0100
     1.2 +++ b/src/Provers/ind.ML	Mon Jan 24 18:15:19 2005 +0100
     1.3 @@ -25,7 +25,6 @@
     1.4  local open Ind_Data in
     1.5  
     1.6  val _$(_$Var(a_ixname,aT)) = concl_of spec;
     1.7 -val a_name = implode(tl(explode(Syntax.string_of_vname a_ixname)));
     1.8  
     1.9  fun add_term_frees tsig =
    1.10  let fun add(tm, vars) = case tm of
    1.11 @@ -37,7 +36,7 @@
    1.12  in add end;
    1.13  
    1.14  
    1.15 -fun qnt_tac i = fn (tac,var) => tac THEN res_inst_tac [(a_name,var)] spec i;
    1.16 +fun qnt_tac i = fn (tac,var) => tac THEN Tactic.res_inst_tac' [(a_ixname,var)] spec i;
    1.17  
    1.18  (*Generalizes over all free variables, with the named var outermost.*)
    1.19  fun all_frees_tac (var:string) i thm = 
     2.1 --- a/src/ZF/Tools/induct_tacs.ML	Mon Jan 24 18:12:22 2005 +0100
     2.2 +++ b/src/ZF/Tools/induct_tacs.ML	Mon Jan 24 18:15:19 2005 +0100
     2.3 @@ -13,8 +13,8 @@
     2.4    val induct_tac: string -> int -> tactic
     2.5    val exhaust_tac: string -> int -> tactic
     2.6    val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
     2.7 -  val rep_datatype: xstring * Args.src list -> xstring * Args.src list ->
     2.8 -    (xstring * Args.src list) list -> (xstring * Args.src list) list -> theory -> theory
     2.9 +  val rep_datatype: thmref * Args.src list -> thmref * Args.src list ->
    2.10 +    (thmref * Args.src list) list -> (thmref * Args.src list) list -> theory -> theory
    2.11    val setup: (theory -> theory) list
    2.12  end;
    2.13  
    2.14 @@ -115,11 +115,8 @@
    2.15          (case prems_of rule of
    2.16               [] => error "induction is not available for this datatype"
    2.17             | major::_ => FOLogic.dest_Trueprop major)
    2.18 -    val ind_vname = Syntax.string_of_vname ixn
    2.19 -    val vname' = (*delete leading question mark*)
    2.20 -        String.substring (ind_vname, 1, size ind_vname-1)
    2.21    in
    2.22 -    eres_inst_tac [(vname',var)] rule i state
    2.23 +    Tactic.eres_inst_tac' [(ixn, var)] rule i state
    2.24    end
    2.25    handle Find_tname msg =>
    2.26              if exh then (*try boolean case analysis instead*)