src/Provers/ind.ML
changeset 15462 b4208fbf9439
parent 14772 c52060b69a8c
child 15570 8d8c70b41bab
     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 =