# HG changeset patch
# User wenzelm
# Date 954532551 -7200
# Node ID 2f699cd7b8d7bd5a63399e0bc1ef8c97fcd85116
# Parent  3f34637cb9c0af76a7d255aa56a4f7a459849984
fixed indexing of elim rules;

diff -r 3f34637cb9c0 -r 2f699cd7b8d7 src/Pure/Isar/net_rules.ML
--- 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;