--- a/src/HOL/UNITY/Comp/AllocBase.ML	Mon May 13 13:22:15 2002 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.ML	Mon May 13 15:27:28 2002 +0200
@@ -56,7 +56,7 @@
 
 Goal "bag_of (sublist l A) = \
 \     (\\<Sum>i: A Int lessThan (length l). {# l!i #})";
-by (rev_induct_tac "l" 1);
+by (res_inst_tac [("xs","l")] rev_induct 1);
 by (Simp_tac 1);
 by (asm_simp_tac
     (simpset() addsimps [sublist_append, Int_insert_right, lessThan_Suc,