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*)