changeset 11693 | 63b0b2ec5830 |
parent 8807 | 0046be1769f9 |
child 11776 | d4f9de0bde28 |
--- a/src/Pure/Isar/net_rules.ML Thu Oct 04 23:27:01 2001 +0200 +++ b/src/Pure/Isar/net_rules.ML Thu Oct 04 23:27:42 2001 +0200 @@ -69,7 +69,7 @@ (* intro/elim rules *) val init_intro = init Thm.eq_thm Thm.concl_of; -val init_elim = init Thm.eq_thm (Logic.strip_assums_concl o Thm.major_prem_of); +val init_elim = init Thm.eq_thm Thm.major_prem_of; end;