# HG changeset patch
# User wenzelm
# Date 1257089011 -3600
# Node ID 69531a7b55b694a6719365de1b521b9669118ffc
# Parent  470a7b233ee5022b51b8a263fb1638e7a7e6cd32
tuned signature;

diff -r 470a7b233ee5 -r 69531a7b55b6 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Sun Nov 01 15:44:26 2009 +0100
+++ b/src/Pure/Isar/context_rules.ML	Sun Nov 01 16:23:31 2009 +0100
@@ -7,8 +7,7 @@
 
 signature CONTEXT_RULES =
 sig
-  type netpair
-  type T
+  type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net
   val netpair_bang: Proof.context -> netpair
   val netpair: Proof.context -> netpair
   val orderlist: ((int * int) * 'a) list -> 'a list
@@ -65,7 +64,7 @@
 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
+datatype rules = Rules of
  {next: int,
   rules: (int * ((int * bool) * thm)) list,
   netpairs: netpair list,
@@ -92,7 +91,7 @@
 
 structure Rules = GenericDataFun
 (
-  type T = T;
+  type T = rules;
   val empty = make_rules ~1 [] empty_netpairs ([], []);
   val extend = I;