# HG changeset patch
# User wenzelm
# Date 1237295360 -3600
# Node ID 2ef9892114fd43c7cd7447d0ce436f0c7ff26088
# Parent  a28d83e903ce8f1c107151f9917cb7807e80e8ca
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);

diff -r a28d83e903ce -r 2ef9892114fd src/Provers/blast.ML
--- a/src/Provers/blast.ML	Tue Mar 17 13:33:21 2009 +0100
+++ b/src/Provers/blast.ML	Tue Mar 17 14:09:20 2009 +0100
@@ -564,11 +564,11 @@
       (Const ("*Goal*", _) $ G) =>
         let val pG = mk_Trueprop (toTerm 2 G)
             val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps
-        in  map (fromIntrRule thy vars o #2) (Tactic.orderlist intrs)  end
+        in  map (fromIntrRule thy vars o #2) (order_list intrs)  end
     | _ =>
         let val pP = mk_Trueprop (toTerm 3 P)
             val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps
-        in  map_filter (fromRule thy vars o #2) (Tactic.orderlist elims)  end;
+        in  map_filter (fromRule thy vars o #2) (order_list elims)  end;
 
 
 (*Normalize a branch--for tracing*)
diff -r a28d83e903ce -r 2ef9892114fd src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Mar 17 13:33:21 2009 +0100
+++ b/src/Provers/classical.ML	Tue Mar 17 14:09:20 2009 +0100
@@ -688,7 +688,7 @@
 (*version of bimatch_from_nets_tac that only applies rules that
   create precisely n subgoals.*)
 fun n_bimatch_from_nets_tac n =
-    biresolution_from_nets_tac (Tactic.orderlist o List.filter (nsubgoalsP n)) true;
+    biresolution_from_nets_tac (order_list o List.filter (nsubgoalsP n)) true;
 
 fun eq_contr_tac i = ematch_tac [not_elim] i  THEN  eq_assume_tac i;
 val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
diff -r a28d83e903ce -r 2ef9892114fd src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Mar 17 13:33:21 2009 +0100
+++ b/src/Pure/library.ML	Tue Mar 17 14:09:20 2009 +0100
@@ -211,6 +211,9 @@
   val sort_distinct: ('a * 'a -> order) -> 'a list -> 'a list
   val sort_strings: string list -> string list
   val sort_wrt: ('a -> string) -> 'a list -> 'a list
+  val tag_list: int -> 'a list -> (int * 'a) list
+  val untag_list: (int * 'a) list -> 'a list
+  val order_list: (int * 'a) list -> 'a list
 
   (*random numbers*)
   exception RANDOM
@@ -1015,6 +1018,23 @@
 fun sort_wrt sel xs = sort (string_ord o pairself sel) xs;
 
 
+(* items tagged by integer index *)
+
+(*insert tags*)
+fun tag_list k [] = []
+  | tag_list k (x :: xs) = (k, x) :: tag_list (k + 1) xs;
+
+(*remove tags and suppress duplicates -- list is assumed sorted!*)
+fun untag_list [] = []
+  | untag_list [(k: int, x)] = [x]
+  | untag_list ((k, x) :: (rest as (k', x') :: _)) =
+      if k = k' then untag_list rest
+      else x :: untag_list rest;
+
+(*return list elements in original order*)
+fun order_list list = untag_list (sort (int_ord o pairself fst) list);
+
+
 
 (** random numbers **)
 
diff -r a28d83e903ce -r 2ef9892114fd src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Tue Mar 17 13:33:21 2009 +0100
+++ b/src/Pure/tactic.ML	Tue Mar 17 14:09:20 2009 +0100
@@ -66,8 +66,6 @@
   val innermost_params: int -> thm -> (string * typ) list
   val term_lift_inst_rule:
     thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm
-  val untaglist: (int * 'a) list -> 'a list
-  val orderlist: (int * 'a) list -> 'a list
   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
@@ -264,20 +262,6 @@
 
 (** To preserve the order of the rules, tag them with increasing integers **)
 
-(*insert tags*)
-fun taglist k [] = []
-  | taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
-
-(*remove tags and suppress duplicates -- list is assumed sorted!*)
-fun untaglist [] = []
-  | untaglist [(k:int,x)] = [x]
-  | untaglist ((k,x) :: (rest as (k',x')::_)) =
-      if k=k' then untaglist rest
-      else    x :: untaglist rest;
-
-(*return list elements in original order*)
-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
@@ -288,7 +272,7 @@
 
 (*build a pair of nets for biresolution*)
 fun build_netpair netpair brls =
-    fold_rev insert_tagged_brl (taglist 1 brls) netpair;
+    fold_rev insert_tagged_brl (tag_list 1 brls) netpair;
 
 (*delete one kbrl from the pair of nets*)
 fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
@@ -314,8 +298,8 @@
       in PRIMSEQ (biresolution match (order kbrls) i) end);
 
 (*versions taking pre-built nets.  No filtering of brls*)
-val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false;
-val bimatch_from_nets_tac   = biresolution_from_nets_tac orderlist true;
+val biresolve_from_nets_tac = biresolution_from_nets_tac order_list false;
+val bimatch_from_nets_tac   = biresolution_from_nets_tac order_list true;
 
 (*fast versions using nets internally*)
 val net_biresolve_tac =
@@ -332,7 +316,7 @@
 
 (*build a net of rules for resolution*)
 fun build_net rls =
-  fold_rev insert_krl (taglist 1 rls) Net.empty;
+  fold_rev insert_krl (tag_list 1 rls) Net.empty;
 
 (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
 fun filt_resolution_from_net_tac match pred net =
@@ -342,7 +326,7 @@
       in
          if pred krls
          then PRIMSEQ
-                (biresolution match (map (pair false) (orderlist krls)) i)
+                (biresolution match (map (pair false) (order_list krls)) i)
          else no_tac
       end);