--- a/src/HOL/ex/Recdef.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/ex/Recdef.ML Wed Dec 24 10:02:30 1997 +0100
@@ -24,7 +24,7 @@
goal thy "g x < Suc x";
by (res_inst_tac [("u","x")] g.induct 1);
-by (Auto_tac());
+by Auto_tac;
by (trans_tac 1);
qed "g_terminates";