# HG changeset patch
# User wenzelm
# Date 1006995098 -3600
# Node ID b4e706774e961defe02f691b8abe8b344c9d4a84
# Parent  4966dae8fa62770ea9134a7e057cae2df2f576d0
export primitive netpairs;
activate attributes;

diff -r 4966dae8fa62 -r b4e706774e96 src/Pure/Isar/rule_context.ML
--- a/src/Pure/Isar/rule_context.ML	Thu Nov 29 01:51:06 2001 +0100
+++ b/src/Pure/Isar/rule_context.ML	Thu Nov 29 01:51:38 2001 +0100
@@ -9,6 +9,7 @@
 
 signature RULE_CONTEXT =
 sig
+  type netpair
   type T
   val print_global_rules: theory -> unit
   val print_local_rules: Proof.context -> unit
@@ -32,6 +33,8 @@
   val elim_query_local: int option -> Proof.context attribute
   val dest_query_local: int option -> Proof.context attribute
   val rule_del_local: Proof.context attribute
+  val netpairs: Proof.context -> netpair list
+  val orderlist: ((int * int) * 'a) list -> 'a list
   val setup: (theory -> theory) list
 end;
 
@@ -64,13 +67,13 @@
 
 (* netpairs *)
 
-type net = ((int * int) * (bool * thm)) Net.net;
-val empty_netpairs = replicate (length rule_indexes) (Net.empty: net, Net.empty: net);
+type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net;
+val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty);
 
 datatype T = Rules of
  {next: int,
   rules: (int * ((int * bool) * thm)) list,
-  netpairs: (net * net) list,
+  netpairs: netpair list,
   wrappers: ((bool * ((int -> tactic) -> int -> tactic)) * stamp) list};
 
 fun make_rules next rules netpairs wrappers =
@@ -207,11 +210,19 @@
 
 
 
+(** retrieving rules **)
+
+fun netpairs ctxt = let val Rules {netpairs, ...} = LocalRules.get ctxt in netpairs end;
+
+fun orderlist brls =
+  map snd (sort (prod_ord int_ord int_ord o pairself fst) brls);
+
+
+
 (** theory setup **)
 
 val setup =
- [GlobalRules.init, LocalRules.init
-  (*FIXME Attrib.add_attributes rule_atts*)];
+ [GlobalRules.init, LocalRules.init, Attrib.add_attributes rule_atts];
 
 
 end;