# HG changeset patch
# User wenzelm
# Date 1006991074 -3600
# Node ID 6e70d870ddf08222fcc8ad409be4d03f24858e25
# Parent  cb3ea5750c3b0a29c49992f1952fed11bf686ac6
general type of delete_tagged_brl;
tuned;

diff -r cb3ea5750c3b -r 6e70d870ddf0 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Nov 29 00:43:39 2001 +0100
+++ b/src/Pure/tactic.ML	Thu Nov 29 00:44:34 2001 +0100
@@ -54,12 +54,12 @@
   val forward_tac       : thm list -> int -> tactic
   val forw_inst_tac     : (string*string)list -> thm -> int -> tactic
   val ftac              : thm -> int ->tactic
-  val insert_tagged_brl : ('a*(bool*thm)) *
-                          (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
-                          ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
-  val delete_tagged_brl : (bool*thm) *
-                         ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) ->
-                    (int*(bool*thm))Net.net * (int*(bool*thm))Net.net
+  val insert_tagged_brl : ('a * (bool * thm)) *
+    (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) ->
+      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
+  val delete_tagged_brl : (bool * thm) *
+    (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) ->
+      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
   val is_fact           : thm -> bool
   val lessb             : (bool * thm) * (bool * thm) -> bool
   val lift_inst_rule    : thm * int * (string*string)list * thm -> thm
@@ -399,28 +399,27 @@
 fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls);
 
 (*insert one tagged brl into the pair of nets*)
-fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =
-    if eres then
-        case prems_of th of
-            prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false))
-          | [] => error"insert_tagged_brl: elimination rule with no premises"
-    else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
+fun insert_tagged_brl (kbrl as (k, (eres, th)), (inet, enet)) =
+  if eres then
+    (case try Thm.major_prem_of th of
+      Some prem => (inet, Net.insert_term ((prem, kbrl), enet, K false))
+    | None => error "insert_tagged_brl: elimination rule with no premises")
+  else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
 
 (*build a pair of nets for biresolution*)
 fun build_netpair netpair brls =
     foldr insert_tagged_brl (taglist 1 brls, netpair);
 
-(*delete one kbrl from the pair of nets;
-  we don't know the value of k, so we use 0 and ignore it in the comparison*)
+(*delete one kbrl from the pair of nets*)
 local
-  fun eq_kbrl ((k,(eres,th)), (k',(eres',th'))) = eq_thm (th,th')
+  fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = eq_thm (th, th')
 in
-fun delete_tagged_brl (brl as (eres,th), (inet,enet)) =
-    if eres then
-        case prems_of th of
-            prem::_ => (inet, Net.delete_term ((prem, (0,brl)), enet, eq_kbrl))
-          | []      => (inet,enet)     (*no major premise: ignore*)
-    else (Net.delete_term ((concl_of th, (0,brl)), inet, eq_kbrl), enet);
+fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
+  if eres then
+    (case try Thm.major_prem_of th of
+      Some prem => (inet, Net.delete_term ((prem, ((), brl)), enet, eq_kbrl))
+    | None => (inet, enet))  (*no major premise: ignore*)
+  else (Net.delete_term ((Thm.concl_of th, ((), brl)), inet, eq_kbrl), enet);
 end;