# HG changeset patch
# User paulson
# Date 861092354 -7200
# Node ID 69def2a31fad792ba0a8dc9f8f93e0e74c9c77e7
# Parent  5d2e0865ecf3f89e8eeddec97b9e3d485cf26b45
An extra call to blast_tac (illustrating a need for type instantiation)

diff -r 5d2e0865ecf3 -r 69def2a31fad src/HOL/ex/Simult.ML
--- a/src/HOL/ex/Simult.ML	Tue Apr 15 10:18:01 1997 +0200
+++ b/src/HOL/ex/Simult.ML	Tue Apr 15 10:19:14 1997 +0200
@@ -74,8 +74,11 @@
 by (rtac (ballI RS TF_induct_lemma) 1);
 by (etac TF_induct 1);
 by (rewrite_goals_tac TF_Rep_defs);
-by (ALLGOALS (fast_tac (!claset addIs prems)));
-(*29 secs??*)
+	(*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)));
 qed "Tree_Forest_induct";
 
 (*Induction for the abstract types 'a tree, 'a forest*)