1.1 --- a/src/HOL/Induct/Simult.ML	Wed Aug 19 10:28:25 1998 +0200
     1.2 +++ b/src/HOL/Induct/Simult.ML	Wed Aug 19 10:29:01 1998 +0200
     1.3 @@ -72,11 +72,7 @@
     1.4  by (rtac (ballI RS TF_induct_lemma) 1);
     1.5  by (etac TF_induct 1);
     1.6  by (rewrite_goals_tac TF_Rep_defs);
     1.7 -	(*Blast_tac needs this type instantiation in order to preserve the
     1.8 -          right overloading of equality.  The injectiveness properties for
     1.9 -          type 'a item hold only for set types.*)
    1.10 -val PartE' = read_instantiate [("'a", "?'c set")] PartE;
    1.11 -by (ALLGOALS (blast_tac (claset() addSEs [PartE'] addIs prems)));
    1.12 +by (ALLGOALS (blast_tac (claset() addIs prems)));
    1.13  qed "Tree_Forest_induct";
    1.14  
    1.15  (*Induction for the abstract types 'a tree, 'a forest*)