diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/TLA/Inc/Inc.ML
--- a/src/HOL/TLA/Inc/Inc.ML	Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/TLA/Inc/Inc.ML	Wed Dec 24 10:02:30 1997 +0100
@@ -171,7 +171,7 @@
   (fn _ => [auto_tac (Inc_css addSIs2 [(temp_mp N2_leadsto_a) RSN(2,leadsto_init)]),
 	    rewrite_goals_tac (Init_def::action_rews),
 	    pcount.induct_tac "pc2 (fst_st sigma)" 1,
-	    Auto_tac()
+	    Auto_tac
 	   ]);
 
 (* Now prove that the first component will eventually reach pc1 = b from pc1 = a *)
@@ -217,7 +217,7 @@
   (fn _ => [auto_tac (Inc_css addSIs2 [(temp_mp N1_leadsto_b) RSN(2,leadsto_init)]),
 	    rewrite_goals_tac (Init_def::action_rews),
 	    pcount.induct_tac "pc1 (fst_st sigma)" 1,
-	    Auto_tac()
+	    Auto_tac
 	   ]);
 
 qed_goal "N1_enabled_at_b" Inc.thy