| changeset 5983 | 79e301a6a51b |
| parent 5521 | 7970832271cc |
| child 7499 | 23e090051cb8 |
--- a/src/HOL/MiniML/Instance.ML Fri Nov 27 16:54:59 1998 +0100 +++ b/src/HOL/MiniML/Instance.ML Fri Nov 27 17:00:30 1998 +0100 @@ -90,7 +90,6 @@ \ bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch"; by (induct_tac "sch" 1); by Auto_tac; -by (ALLGOALS trans_tac); val aux2 = result () RS mp;