diff -r 8d63ff01d37e -r 54785105178c src/HOL/IMP/Transition.ML
--- a/src/HOL/IMP/Transition.ML	Mon Jun 16 14:25:33 1997 +0200
+++ b/src/HOL/IMP/Transition.ML	Tue Jun 17 09:01:56 1997 +0200
@@ -128,7 +128,7 @@
 goal Transition.thy
  "!!c1. (c1,s1) -*-> (SKIP,s2) ==> \
 \ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";
-by (etac converse_rtrancl_induct2 1);
+by (etac inverse_rtrancl_induct2 1);
 by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
 by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
 qed_spec_mp "my_lemma1";