src/HOL/MiniML/Type.ML
changeset 14401 477380c74c1d
parent 13630 a013a9dd370f
     1.1 --- a/src/HOL/MiniML/Type.ML	Thu Feb 19 17:57:54 2004 +0100
     1.2 +++ b/src/HOL/MiniML/Type.ML	Thu Feb 19 18:24:08 2004 +0100
     1.3 @@ -373,7 +373,7 @@
     1.4  Addsimps [bound_tv_subst_scheme];
     1.5  
     1.6  Goal "!!A::type_scheme list. bound_tv ($ S A) = bound_tv A";
     1.7 -by (rtac list.induct 1);
     1.8 +by (rtac (thm"list.induct") 1);
     1.9  by (Simp_tac 1);
    1.10  by (Asm_simp_tac 1);
    1.11  qed "bound_tv_subst_scheme_list";
    1.12 @@ -627,7 +627,7 @@
    1.13  Addsimps [subst_TVar_scheme];
    1.14  
    1.15  Goal "!!A::type_scheme list. $ TVar A = A";
    1.16 -by (rtac list.induct 1);
    1.17 +by (rtac (thm"list.induct") 1);
    1.18  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [app_subst_list])));
    1.19  qed "subst_TVar_scheme_list";
    1.20