Eliminated hack for deleting leading question mark from induction
variable name.
--- a/src/Provers/ind.ML Mon Jan 24 18:12:22 2005 +0100
+++ b/src/Provers/ind.ML Mon Jan 24 18:15:19 2005 +0100
@@ -25,7 +25,6 @@
local open Ind_Data in
val _$(_$Var(a_ixname,aT)) = concl_of spec;
-val a_name = implode(tl(explode(Syntax.string_of_vname a_ixname)));
fun add_term_frees tsig =
let fun add(tm, vars) = case tm of
@@ -37,7 +36,7 @@
in add end;
-fun qnt_tac i = fn (tac,var) => tac THEN res_inst_tac [(a_name,var)] spec i;
+fun qnt_tac i = fn (tac,var) => tac THEN Tactic.res_inst_tac' [(a_ixname,var)] spec i;
(*Generalizes over all free variables, with the named var outermost.*)
fun all_frees_tac (var:string) i thm =
--- a/src/ZF/Tools/induct_tacs.ML Mon Jan 24 18:12:22 2005 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Mon Jan 24 18:15:19 2005 +0100
@@ -13,8 +13,8 @@
val induct_tac: string -> int -> tactic
val exhaust_tac: string -> int -> tactic
val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
- val rep_datatype: xstring * Args.src list -> xstring * Args.src list ->
- (xstring * Args.src list) list -> (xstring * Args.src list) list -> theory -> theory
+ val rep_datatype: thmref * Args.src list -> thmref * Args.src list ->
+ (thmref * Args.src list) list -> (thmref * Args.src list) list -> theory -> theory
val setup: (theory -> theory) list
end;
@@ -115,11 +115,8 @@
(case prems_of rule of
[] => error "induction is not available for this datatype"
| major::_ => FOLogic.dest_Trueprop major)
- val ind_vname = Syntax.string_of_vname ixn
- val vname' = (*delete leading question mark*)
- String.substring (ind_vname, 1, size ind_vname-1)
in
- eres_inst_tac [(vname',var)] rule i state
+ Tactic.eres_inst_tac' [(ixn, var)] rule i state
end
handle Find_tname msg =>
if exh then (*try boolean case analysis instead*)