src/Provers/ind.ML
changeset 1512 ce37c64244c0
parent 0 a5a9c433f639
child 4452 b2ee34200dab
     1.1 --- a/src/Provers/ind.ML	Fri Feb 16 17:24:51 1996 +0100
     1.2 +++ b/src/Provers/ind.ML	Fri Feb 16 18:00:47 1996 +0100
     1.3 @@ -40,22 +40,23 @@
     1.4  fun qnt_tac i = fn (tac,var) => tac THEN res_inst_tac [(a_name,var)] spec i;
     1.5  
     1.6  (*Generalizes over all free variables, with the named var outermost.*)
     1.7 -fun all_frees_tac (var:string) i = Tactic(fn thm =>
     1.8 +fun all_frees_tac (var:string) i thm = 
     1.9      let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm)));
    1.10          val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]);
    1.11          val frees' = sort(op>)(frees \ var) @ [var]
    1.12 -    in tapply(foldl (qnt_tac i) (all_tac,frees'), thm) end);
    1.13 +    in foldl (qnt_tac i) (all_tac,frees') thm end;
    1.14  
    1.15  fun REPEAT_SIMP_TAC simp_tac n i =
    1.16 -let fun repeat thm = tapply(COND (has_fewer_prems n) all_tac
    1.17 -	let val k = length(prems_of thm)
    1.18 -	in simp_tac i THEN COND (has_fewer_prems k) (Tactic repeat) all_tac
    1.19 -	end, thm)
    1.20 -in Tactic repeat end;
    1.21 +let fun repeat thm = 
    1.22 +        (COND (has_fewer_prems n) all_tac
    1.23 +	 let val k = nprems_of thm
    1.24 +	 in simp_tac i THEN COND (has_fewer_prems k) repeat all_tac end)
    1.25 +	thm
    1.26 +in repeat end;
    1.27  
    1.28 -fun ALL_IND_TAC sch simp_tac i = Tactic(fn thm => tapply(
    1.29 -	resolve_tac [sch] i THEN
    1.30 -	REPEAT_SIMP_TAC simp_tac (length(prems_of thm)) i, thm));
    1.31 +fun ALL_IND_TAC sch simp_tac i thm = 
    1.32 +	(resolve_tac [sch] i THEN
    1.33 +	 REPEAT_SIMP_TAC simp_tac (nprems_of thm) i) thm;
    1.34  
    1.35  fun IND_TAC sch simp_tac var =
    1.36  	all_frees_tac var THEN' ALL_IND_TAC sch simp_tac;