diff -r 58b6f99dd5a9 -r a466c687c726 src/HOLCF/IOA/ex/TrivEx2.ML
--- a/src/HOLCF/IOA/ex/TrivEx2.ML	Tue Mar 28 12:28:24 2000 +0200
+++ b/src/HOLCF/IOA/ex/TrivEx2.ML	Tue Mar 28 17:31:36 2000 +0200
@@ -22,9 +22,8 @@
 by (rtac imp_conj_lemma 1);
 by (simp_tac (simpset() addsimps [trans_of_def,
         C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
+by (induct_tac "a" 1);
 by (simp_tac (simpset() addsimps [h_abs_def]) 1);
-by (induct_tac "a" 1);
-by Auto_tac;
 qed"h_abs_is_abstraction";