author | oheimb |
Mon, 21 Sep 1998 23:13:28 +0200 | |
changeset 5522 | 982c710450c6 |
parent 5521 | 7970832271cc |
child 5523 | dc8cdc192cd0 |
--- a/src/HOL/MiniML/Generalize.ML Mon Sep 21 23:12:31 1998 +0200 +++ b/src/HOL/MiniML/Generalize.ML Mon Sep 21 23:13:28 1998 +0200 @@ -64,7 +64,7 @@ Goalw [gen_ML_def] "gen A t = gen_ML A t"; by (induct_tac "t" 1); -by (simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1); + by (simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1); by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1); qed "gen_eq_gen_ML";