export eq_brl;
authorwenzelm
Wed Jul 13 16:07:30 2005 +0200 (2005-07-13)
changeset 168098ca51a846576
parent 16808 644fc45c7292
child 16810 2406588f99cb
export eq_brl;
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Wed Jul 13 16:07:29 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Wed Jul 13 16:07:30 2005 +0200
     1.3 @@ -106,6 +106,7 @@
     1.4    include BASIC_TACTIC
     1.5    val innermost_params: int -> thm -> (string * typ) list
     1.6    val untaglist: (int * 'a) list -> 'a list
     1.7 +  val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool
     1.8    val orderlist: (int * 'a) list -> 'a list
     1.9    val rewrite: bool -> thm list -> cterm -> thm
    1.10    val simplify: bool -> thm list -> thm -> thm
    1.11 @@ -437,26 +438,24 @@
    1.12  fun insert_tagged_brl (kbrl as (k, (eres, th)), (inet, enet)) =
    1.13    if eres then
    1.14      (case try Thm.major_prem_of th of
    1.15 -      SOME prem => (inet, Net.insert_term ((prem, kbrl), enet, K false))
    1.16 +      SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet)
    1.17      | NONE => error "insert_tagged_brl: elimination rule with no premises")
    1.18 -  else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
    1.19 +  else (Net.insert_term (K false) (concl_of th, kbrl) inet, enet);
    1.20  
    1.21  (*build a pair of nets for biresolution*)
    1.22  fun build_netpair netpair brls =
    1.23      foldr insert_tagged_brl netpair (taglist 1 brls);
    1.24  
    1.25  (*delete one kbrl from the pair of nets*)
    1.26 -local
    1.27 -  fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th')
    1.28 -in
    1.29 +fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th')
    1.30 +
    1.31  fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
    1.32    (if eres then
    1.33      (case try Thm.major_prem_of th of
    1.34 -      SOME prem => (inet, Net.delete_term ((prem, ((), brl)), enet, eq_kbrl))
    1.35 +      SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet)
    1.36      | NONE => (inet, enet))  (*no major premise: ignore*)
    1.37 -  else (Net.delete_term ((Thm.concl_of th, ((), brl)), inet, eq_kbrl), enet))
    1.38 +  else (Net.delete_term eq_kbrl (Thm.concl_of th, ((), brl)) inet, enet))
    1.39    handle Net.DELETE => (inet,enet);
    1.40 -end;
    1.41  
    1.42  
    1.43  (*biresolution using a pair of nets rather than rules.
    1.44 @@ -486,7 +485,7 @@
    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 ((concl_of th, krl), net, K false);
    1.49 +    Net.insert_term (K false) (concl_of th, krl) net;
    1.50  
    1.51  (*build a net of rules for resolution*)
    1.52  fun build_net rls =