src/Pure/Isar/context_rules.ML
changeset 33519 e31a85f92ce9
parent 33370 69531a7b55b6
child 36950 75b8f26f2f07
     1.1 --- a/src/Pure/Isar/context_rules.ML	Sun Nov 08 16:28:18 2009 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Sun Nov 08 16:30:41 2009 +0100
     1.3 @@ -89,13 +89,13 @@
     1.4      else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
     1.5    end;
     1.6  
     1.7 -structure Rules = GenericDataFun
     1.8 +structure Rules = Generic_Data
     1.9  (
    1.10    type T = rules;
    1.11    val empty = make_rules ~1 [] empty_netpairs ([], []);
    1.12    val extend = I;
    1.13 -
    1.14 -  fun merge _ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
    1.15 +  fun merge
    1.16 +    (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
    1.17        Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
    1.18      let
    1.19        val wrappers =