src/Pure/Isar/locale.ML
changeset 33519 e31a85f92ce9
parent 33278 ba9f52f56356
child 33522 737589bb9bb8
     1.1 --- a/src/Pure/Isar/locale.ML	Sun Nov 08 16:28:18 2009 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Sun Nov 08 16:30:41 2009 +0100
     1.3 @@ -188,12 +188,12 @@
     1.4  
     1.5  datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
     1.6  
     1.7 -structure Identifiers = GenericDataFun
     1.8 +structure Identifiers = Generic_Data
     1.9  (
    1.10    type T = (string * term list) list delayed;
    1.11    val empty = Ready [];
    1.12    val extend = I;
    1.13 -  fun merge _ = ToDo;
    1.14 +  val merge = ToDo;
    1.15  );
    1.16  
    1.17  fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
    1.18 @@ -569,12 +569,12 @@
    1.19  
    1.20  (* Storage for witnesses, intro and unfold rules *)
    1.21  
    1.22 -structure Thms = GenericDataFun
    1.23 +structure Thms = Generic_Data
    1.24  (
    1.25    type T = thm list * thm list * thm list;
    1.26    val empty = ([], [], []);
    1.27    val extend = I;
    1.28 -  fun merge _ ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
    1.29 +  fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
    1.30     (Thm.merge_thms (witnesses1, witnesses2),
    1.31      Thm.merge_thms (intros1, intros2),
    1.32      Thm.merge_thms (unfolds1, unfolds2));