# HG changeset patch
# User paulson
# Date 932391102 -7200
# Node ID 895c7c1e56ba0c50971f5c1df70c76091640a18f
# Parent  d1b7a2372b311fe3e8b9769cf5d5adde85c4c35b
deleted a reference to "nat", now erroneous because "nat" is a function

diff -r d1b7a2372b31 -r 895c7c1e56ba src/HOL/MiniML/Generalize.ML
--- a/src/HOL/MiniML/Generalize.ML	Mon Jul 19 15:30:59 1999 +0200
+++ b/src/HOL/MiniML/Generalize.ML	Mon Jul 19 15:31:42 1999 +0200
@@ -56,10 +56,7 @@
 
 Goal "new_tv n t --> new_tv n (gen A t)";
 by (induct_tac "t" 1);
-by (Simp_tac 1);
-by (case_tac "nat : free_tv A" 1);
-by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
+by Auto_tac;
 qed_spec_mp "new_tv_compatible_gen";
 
 Goalw [gen_ML_def] "gen A t = gen_ML A t";