# HG changeset patch
# User nipkow
# Date 877003978 -7200
# Node ID 7cd00b628e32edc1fb59f38c1acd8b3d3b91fe3c
# Parent  ee8ebb74ec00db3d8945c41c83130ae69a9b7add
Simplified proof because of better simplifier.

diff -r ee8ebb74ec00 -r 7cd00b628e32 src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Thu Oct 16 14:12:15 1997 +0200
+++ b/src/HOL/MiniML/Type.ML	Thu Oct 16 14:12:58 1997 +0200
@@ -26,7 +26,6 @@
 by (typ.induct_tac "t'" 1);
  by (Simp_tac 1);
 by (Asm_full_simp_tac 1);
-by (Fast_tac 1);
 qed_spec_mp "mk_scheme_injective";
 
 goal thy "!!t. free_tv (mk_scheme t) = free_tv t";