# HG changeset patch
# User paulson
# Date 903515341 -7200
# Node ID 22c195854229e0f8c572ff7fa4a189a3114c8cfb
# Parent  9f999cf852e0afbf0432fb21aec33c0d838a5c7e
Deleted obsolete declaration of PartE'

diff -r 9f999cf852e0 -r 22c195854229 src/HOL/Induct/Simult.ML
--- 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*)