deleted a reference to "nat", now erroneous because "nat" is a function
authorpaulson
Mon, 19 Jul 1999 15:31:42 +0200
changeset 7036 895c7c1e56ba
parent 7035 d1b7a2372b31
child 7037 77d596a5ffae
deleted a reference to "nat", now erroneous because "nat" is a function
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";