src/Pure/Isar/context_rules.ML
changeset 33370 69531a7b55b6
parent 33369 470a7b233ee5
child 33519 e31a85f92ce9
     1.1 --- a/src/Pure/Isar/context_rules.ML	Sun Nov 01 15:44:26 2009 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Sun Nov 01 16:23:31 2009 +0100
     1.3 @@ -7,8 +7,7 @@
     1.4  
     1.5  signature CONTEXT_RULES =
     1.6  sig
     1.7 -  type netpair
     1.8 -  type T
     1.9 +  type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net
    1.10    val netpair_bang: Proof.context -> netpair
    1.11    val netpair: Proof.context -> netpair
    1.12    val orderlist: ((int * int) * 'a) list -> 'a list
    1.13 @@ -65,7 +64,7 @@
    1.14  type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net;
    1.15  val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty);
    1.16  
    1.17 -datatype T = Rules of
    1.18 +datatype rules = Rules of
    1.19   {next: int,
    1.20    rules: (int * ((int * bool) * thm)) list,
    1.21    netpairs: netpair list,
    1.22 @@ -92,7 +91,7 @@
    1.23  
    1.24  structure Rules = GenericDataFun
    1.25  (
    1.26 -  type T = T;
    1.27 +  type T = rules;
    1.28    val empty = make_rules ~1 [] empty_netpairs ([], []);
    1.29    val extend = I;
    1.30