src/Pure/tactic.ML
changeset 23178 07ba6b58b3d2
parent 22583 4b1ecb19b411
child 23223 7791128b39a9
     1.1 --- a/src/Pure/tactic.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Pure/tactic.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -51,11 +51,11 @@
     1.4    val forward_tac       : thm list -> int -> tactic
     1.5    val forw_inst_tac     : (string*string)list -> thm -> int -> tactic
     1.6    val ftac              : thm -> int ->tactic
     1.7 -  val insert_tagged_brl : ('a * (bool * thm)) *
     1.8 -    (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) ->
     1.9 +  val insert_tagged_brl : 'a * (bool * thm) ->
    1.10 +    ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
    1.11        ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
    1.12 -  val delete_tagged_brl : (bool * thm) *
    1.13 -    (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) ->
    1.14 +  val delete_tagged_brl : bool * thm ->
    1.15 +    ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
    1.16        ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
    1.17    val lessb             : (bool * thm) * (bool * thm) -> bool
    1.18    val lift_inst_rule    : thm * int * (string*string)list * thm -> thm
    1.19 @@ -410,7 +410,7 @@
    1.20  fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls);
    1.21  
    1.22  (*insert one tagged brl into the pair of nets*)
    1.23 -fun insert_tagged_brl (kbrl as (k, (eres, th)), (inet, enet)) =
    1.24 +fun insert_tagged_brl (kbrl as (k, (eres, th))) (inet, enet) =
    1.25    if eres then
    1.26      (case try Thm.major_prem_of th of
    1.27        SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet)
    1.28 @@ -419,12 +419,12 @@
    1.29  
    1.30  (*build a pair of nets for biresolution*)
    1.31  fun build_netpair netpair brls =
    1.32 -    foldr insert_tagged_brl netpair (taglist 1 brls);
    1.33 +    fold_rev insert_tagged_brl (taglist 1 brls) netpair;
    1.34  
    1.35  (*delete one kbrl from the pair of nets*)
    1.36  fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
    1.37  
    1.38 -fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
    1.39 +fun delete_tagged_brl (brl as (eres, th)) (inet, enet) =
    1.40    (if eres then
    1.41      (case try Thm.major_prem_of th of
    1.42        SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet)
    1.43 @@ -458,12 +458,12 @@
    1.44  (*** Simpler version for resolve_tac -- only one net, and no hyps ***)
    1.45  
    1.46  (*insert one tagged rl into the net*)
    1.47 -fun insert_krl (krl as (k,th), net) =
    1.48 -    Net.insert_term (K false) (concl_of th, krl) net;
    1.49 +fun insert_krl (krl as (k,th)) =
    1.50 +  Net.insert_term (K false) (concl_of th, krl);
    1.51  
    1.52  (*build a net of rules for resolution*)
    1.53  fun build_net rls =
    1.54 -    foldr insert_krl Net.empty (taglist 1 rls);
    1.55 +  fold_rev insert_krl (taglist 1 rls) Net.empty;
    1.56  
    1.57  (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
    1.58  fun filt_resolution_from_net_tac match pred net =