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