src/Pure/Isar/net_rules.ML

--- a/src/Pure/Isar/net_rules.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/Pure/Isar/net_rules.ML	Tue May 07 14:26:32 2002 +0200
@@ -63,8 +63,8 @@
 
 (* intro/elim rules *)
 
-val intro = init Thm.eq_thm Thm.concl_of;
-val elim = init Thm.eq_thm Thm.major_prem_of;
+val intro = init Drule.eq_thm_prop Thm.concl_of;
+val elim = init Drule.eq_thm_prop Thm.major_prem_of;
 
 
 end;