src/Pure/Isar/net_rules.ML
changeset 13105 3d1e7a199bdc
parent 12385 389d11fb62c8
child 14472 cba7c0a3ffb3
     1.1 --- a/src/Pure/Isar/net_rules.ML	Tue May 07 14:24:30 2002 +0200
     1.2 +++ b/src/Pure/Isar/net_rules.ML	Tue May 07 14:26:32 2002 +0200
     1.3 @@ -63,8 +63,8 @@
     1.4  
     1.5  (* intro/elim rules *)
     1.6  
     1.7 -val intro = init Thm.eq_thm Thm.concl_of;
     1.8 -val elim = init Thm.eq_thm Thm.major_prem_of;
     1.9 +val intro = init Drule.eq_thm_prop Thm.concl_of;
    1.10 +val elim = init Drule.eq_thm_prop Thm.major_prem_of;
    1.11  
    1.12  
    1.13  end;