diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Induct/LList.ML	Wed Dec 24 10:02:30 1997 +0100
@@ -652,7 +652,7 @@
 (*Surprisingly hard to prove.  Used with lfilter*)
 goalw thy [llistD_Fun_def, prod_fun_def]
     "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
-by (Auto_tac());
+by Auto_tac;
 by (rtac image_eqI 1);
 by (fast_tac (claset() addss (simpset())) 1);
 by (blast_tac (claset() addIs [impOfSubs LListD_Fun_mono]) 1);