--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Nov 08 18:43:42 2009 +0100
@@ -63,13 +63,12 @@
reduction_pair : thm
}
-structure Multiset_Setup = TheoryDataFun
+structure Multiset_Setup = Theory_Data
(
type T = multiset_setup option
val empty = NONE
- val copy = I;
val extend = I;
- fun merge _ (v1, v2) = if is_some v2 then v2 else v1
+ fun merge (v1, v2) = if is_some v2 then v2 else v1 (* FIXME prefer v1 !?! *)
)
val multiset_setup = Multiset_Setup.put o SOME