diff -r e28553315355 -r d78cf498a88c src/HOL/Induct/Exp.ML
--- a/src/HOL/Induct/Exp.ML	Fri Sep 26 10:12:04 1997 +0200
+++ b/src/HOL/Induct/Exp.ML	Fri Sep 26 10:21:14 1997 +0200
@@ -80,7 +80,7 @@
 by (Blast_tac 1);
 by (blast_tac (!claset addEs [exec_WHILE_case]) 1);
 by (thin_tac "(?c,s2) -[?ev]-> s3" 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (etac exec_WHILE_case 1);
 by (ALLGOALS Fast_tac);         (*Blast_tac: proof fails*)
 qed "com_Unique";
@@ -197,10 +197,8 @@
 qed "valof_valof";
 
 
-
 (** Equivalence of  VALOF SKIP RESULTIS e  and  e **)
 
-
 goal thy "!!x. (e',s) -|-> (v,s') ==> \
 \              (e' = VALOF SKIP RESULTIS e) --> \
 \              (e, s) -|-> (v,s')";
@@ -218,7 +216,6 @@
 qed "valof_skip";
 
 
-
 (** Equivalence of  VALOF x:=e RESULTIS x  and  e **)
 
 goal thy "!!x. (e',s) -|-> (v,s'') ==> \
@@ -227,7 +224,7 @@
 by (etac eval_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (thin_tac "?PP-->?QQ" 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (Simp_tac 1);
 by (Blast_tac 1); 
 bind_thm ("valof_assign1", refl RSN (2, result() RS mp));