# HG changeset patch
# User wenzelm
# Date 1002230862 -7200
# Node ID 63b0b2ec583096e2388e0ac5d895b0cba0072623
# Parent  6d15ae4b1123e95f4e0c3fa7be24655f4ca282bb
Thm.major_prem_of part of Logic.strip_assums_concl;

diff -r 6d15ae4b1123 -r 63b0b2ec5830 src/Pure/Isar/net_rules.ML
--- 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;