induct_tac -> exhaust_tac in 2 places.

--- a/src/HOL/TLA/Inc/Inc.ML	Wed Jul 22 17:59:49 1998 +0200
+++ b/src/HOL/TLA/Inc/Inc.ML	Fri Jul 24 08:10:04 1998 +0200
@@ -170,7 +170,7 @@
 \  .-> <>($pc2 .= #a)"
   (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,
+	    exhaust_tac "pc2 (fst_st sigma)" 1,
 	    Auto_tac
 	   ]);
 
@@ -216,7 +216,7 @@
 \  .-> <>($pc1 .= #b)"
   (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,
+	    exhaust_tac "pc1 (fst_st sigma)" 1,
 	    Auto_tac
 	   ]);