# HG changeset patch
# User paulson
# Date 1009530655 -3600
# Node ID c198367640f6c233db8fb8b380e8b1559d8f98a5
# Parent  5292f393c64be71b2d75c9d26239fb9eba4fcc24
fixed variable-clash bug in make_elim

diff -r 5292f393c64b -r c198367640f6 src/Provers/make_elim.ML
--- a/src/Provers/make_elim.ML	Thu Dec 27 16:49:15 2001 +0100
+++ b/src/Provers/make_elim.ML	Fri Dec 28 10:10:55 2001 +0100
@@ -34,13 +34,14 @@
 in
 
 fun make_elim rl =
-    let fun making (i,rl) =
-	case compose_extra 2 (cla_dist_concl,i,rl) of
-	    [] => rl
-	  | rl'::_ => making (i+1,rl')
-    in  making (2, hd (compose_extra 1 (rl, 1, revcut_rl)))  end
-    handle THM _ => (*in default, use the previous version, which never fails*)
-             Tactic.make_elim rl;
+    let val revcut_rl' = incr_indexes_wrt [] [] [] [rl] revcut_rl
+        fun making (i,rl) =
+	    case compose_extra 2 (cla_dist_concl,i,rl) of
+		[] => rl     (*terminates by clash of variables!*)
+	      | rl'::_ => making (i+1,rl')
+    in  making (2, hd (compose_extra 1 (rl, 1, revcut_rl')))  end
+    handle (*in default, use the previous version, which never fails*)
+	   THM _ => Tactic.make_elim rl | LIST _ => Tactic.make_elim rl;
 
 end