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