--- a/src/HOL/Algebra/ringsimp.ML Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Sun Nov 08 16:30:41 2009 +0100
@@ -18,7 +18,7 @@
fun struct_eq ((s1: string, ts1), (s2, ts2)) =
(s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
-structure Data = GenericDataFun
+structure Data = Generic_Data
(
type T = ((string * term list) * thm list) list;
(* Algebraic structures:
@@ -26,7 +26,7 @@
identifier and operations identify the structure uniquely. *)
val empty = [];
val extend = I;
- fun merge _ = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop));
+ val merge = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop));
);
fun print_structures ctxt =