--- a/src/HOL/ex/LList.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/ex/LList.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -649,7 +649,7 @@
 goalw thy [llistD_Fun_def, prod_fun_def]
     "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
 by (Auto_tac());
-br image_eqI 1;
+by (rtac image_eqI 1);
 by (fast_tac (!claset addss (!simpset)) 1);
 by (blast_tac (!claset addIs [impOfSubs LListD_Fun_mono]) 1);
 qed "llistD_Fun_mono";