1.1 --- a/src/HOLCF/IOA/ex/TrivEx.ML	Tue Mar 28 12:28:24 2000 +0200
     1.2 +++ b/src/HOLCF/IOA/ex/TrivEx.ML	Tue Mar 28 17:31:36 2000 +0200
     1.3 @@ -22,9 +22,8 @@
     1.4  by (rtac imp_conj_lemma 1);
     1.5  by (simp_tac (simpset() addsimps [trans_of_def,
     1.6          C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
     1.7 +by (induct_tac "a" 1);
     1.8  by (simp_tac (simpset() addsimps [h_abs_def]) 1);
     1.9 -by (induct_tac "a" 1);
    1.10 -by Auto_tac;
    1.11  qed"h_abs_is_abstraction";
    1.12  
    1.13