1.1 --- a/src/Provers/make_elim.ML	Thu Dec 27 16:49:15 2001 +0100
     1.2 +++ b/src/Provers/make_elim.ML	Fri Dec 28 10:10:55 2001 +0100
     1.3 @@ -34,13 +34,14 @@
     1.4  in
     1.5  
     1.6  fun make_elim rl =
     1.7 -    let fun making (i,rl) =
     1.8 -	case compose_extra 2 (cla_dist_concl,i,rl) of
     1.9 -	    [] => rl
    1.10 -	  | rl'::_ => making (i+1,rl')
    1.11 -    in  making (2, hd (compose_extra 1 (rl, 1, revcut_rl)))  end
    1.12 -    handle THM _ => (*in default, use the previous version, which never fails*)
    1.13 -             Tactic.make_elim rl;
    1.14 +    let val revcut_rl' = incr_indexes_wrt [] [] [] [rl] revcut_rl
    1.15 +        fun making (i,rl) =
    1.16 +	    case compose_extra 2 (cla_dist_concl,i,rl) of
    1.17 +		[] => rl     (*terminates by clash of variables!*)
    1.18 +	      | rl'::_ => making (i+1,rl')
    1.19 +    in  making (2, hd (compose_extra 1 (rl, 1, revcut_rl')))  end
    1.20 +    handle (*in default, use the previous version, which never fails*)
    1.21 +	   THM _ => Tactic.make_elim rl | LIST _ => Tactic.make_elim rl;
    1.22  
    1.23  end
    1.24