src/Pure/tactic.ML
changeset 30558 2ef9892114fd
parent 29276 94b1ffec9201
child 31251 6ff48aa6142c
     1.1 --- a/src/Pure/tactic.ML	Tue Mar 17 13:33:21 2009 +0100
     1.2 +++ b/src/Pure/tactic.ML	Tue Mar 17 14:09:20 2009 +0100
     1.3 @@ -66,8 +66,6 @@
     1.4    val innermost_params: int -> thm -> (string * typ) list
     1.5    val term_lift_inst_rule:
     1.6      thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm
     1.7 -  val untaglist: (int * 'a) list -> 'a list
     1.8 -  val orderlist: (int * 'a) list -> 'a list
     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 @@ -264,20 +262,6 @@
    1.13  
    1.14  (** To preserve the order of the rules, tag them with increasing integers **)
    1.15  
    1.16 -(*insert tags*)
    1.17 -fun taglist k [] = []
    1.18 -  | taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
    1.19 -
    1.20 -(*remove tags and suppress duplicates -- list is assumed sorted!*)
    1.21 -fun untaglist [] = []
    1.22 -  | untaglist [(k:int,x)] = [x]
    1.23 -  | untaglist ((k,x) :: (rest as (k',x')::_)) =
    1.24 -      if k=k' then untaglist rest
    1.25 -      else    x :: untaglist rest;
    1.26 -
    1.27 -(*return list elements in original order*)
    1.28 -fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls);
    1.29 -
    1.30  (*insert one tagged brl into the pair of nets*)
    1.31  fun insert_tagged_brl (kbrl as (k, (eres, th))) (inet, enet) =
    1.32    if eres then
    1.33 @@ -288,7 +272,7 @@
    1.34  
    1.35  (*build a pair of nets for biresolution*)
    1.36  fun build_netpair netpair brls =
    1.37 -    fold_rev insert_tagged_brl (taglist 1 brls) netpair;
    1.38 +    fold_rev insert_tagged_brl (tag_list 1 brls) netpair;
    1.39  
    1.40  (*delete one kbrl from the pair of nets*)
    1.41  fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
    1.42 @@ -314,8 +298,8 @@
    1.43        in PRIMSEQ (biresolution match (order kbrls) i) end);
    1.44  
    1.45  (*versions taking pre-built nets.  No filtering of brls*)
    1.46 -val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false;
    1.47 -val bimatch_from_nets_tac   = biresolution_from_nets_tac orderlist true;
    1.48 +val biresolve_from_nets_tac = biresolution_from_nets_tac order_list false;
    1.49 +val bimatch_from_nets_tac   = biresolution_from_nets_tac order_list true;
    1.50  
    1.51  (*fast versions using nets internally*)
    1.52  val net_biresolve_tac =
    1.53 @@ -332,7 +316,7 @@
    1.54  
    1.55  (*build a net of rules for resolution*)
    1.56  fun build_net rls =
    1.57 -  fold_rev insert_krl (taglist 1 rls) Net.empty;
    1.58 +  fold_rev insert_krl (tag_list 1 rls) Net.empty;
    1.59  
    1.60  (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
    1.61  fun filt_resolution_from_net_tac match pred net =
    1.62 @@ -342,7 +326,7 @@
    1.63        in
    1.64           if pred krls
    1.65           then PRIMSEQ
    1.66 -                (biresolution match (map (pair false) (orderlist krls)) i)
    1.67 +                (biresolution match (map (pair false) (order_list krls)) i)
    1.68           else no_tac
    1.69        end);
    1.70