1.1 --- a/src/HOL/MiniML/Instance.ML	Thu Aug 20 16:20:17 1998 +0200
     1.2 +++ b/src/HOL/MiniML/Instance.ML	Thu Aug 20 16:23:43 1998 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4  Goal "new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \
     1.5  \                                                 (bound_typ_inst (%k. TVar (k + n)) sch) = sch";
     1.6  by (induct_tac "sch" 1);
     1.7 -by (simp_tac (simpset() addsimps [leD]) 1);
     1.8 +by (simp_tac (simpset() addsimps [le_def]) 1);
     1.9  by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2]) 1);
    1.10  by (Asm_simp_tac 1);
    1.11  qed_spec_mp "subst_to_scheme_inverse";
    1.12 @@ -97,9 +97,8 @@
    1.13  \     subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
    1.14  \      bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch";
    1.15  by (induct_tac "sch" 1);
    1.16 -by (simp_tac (simpset() addsimps [leD]) 1);
    1.17 -by (Asm_simp_tac 1);
    1.18 -by (asm_full_simp_tac (simpset() addsimps [leD]) 1);
    1.19 +by Auto_tac;
    1.20 +by (ALLGOALS trans_tac);
    1.21  val aux2 = result () RS mp;
    1.22  
    1.23