fixed indexing of elim rules;

--- a/src/Pure/Isar/net_rules.ML	Fri Mar 31 21:55:27 2000 +0200
+++ b/src/Pure/Isar/net_rules.ML	Fri Mar 31 21:55:51 2000 +0200
@@ -37,7 +37,7 @@
   Rules {eq = eq, index = index, rules = rules, next = next, net = net};
 
 fun rules (Rules {rules = rs, ...}) = rs;
-fun may_unify (Rules {net, ...}) tm = Tactic.orderlist (Net.unify_term net tm);
+fun may_unify (Rules {rules, net, ...}) tm = Tactic.orderlist (Net.unify_term net tm);
 
 
 (* build rules *)
@@ -68,7 +68,7 @@
 (* intro/elim rules *)
 
 val init_intro = init Thm.eq_thm Thm.concl_of;
-val init_elim = init Thm.eq_thm Thm.major_prem_of;
+val init_elim = init Thm.eq_thm (Logic.strip_assums_concl o Thm.major_prem_of);
 
 
 end;