| changeset 3897 | 7cd00b628e32 |
| parent 3842 | b55686a7b22c |
| child 3919 | c036caebfc75 |
--- 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";