src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 33522 737589bb9bb8
parent 33351 37ec56ac3fd4
child 33583 b5e0909cd5ea
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -179,14 +179,13 @@
   unrolled_preds: unrolled list Unsynchronized.ref,
   wf_cache: wf_cache Unsynchronized.ref}
 
-structure TheoryData = TheoryDataFun(
+structure TheoryData = Theory_Data(
   type T = {frac_types: (string * (string * string) list) list,
             codatatypes: (string * (string * styp list)) list}
   val empty = {frac_types = [], codatatypes = []}
-  val copy = I
   val extend = I
-  fun merge _ ({frac_types = fs1, codatatypes = cs1},
-               {frac_types = fs2, codatatypes = cs2}) =
+  fun merge ({frac_types = fs1, codatatypes = cs1},
+               {frac_types = fs2, codatatypes = cs2}) : T =
     {frac_types = AList.merge (op =) (op =) (fs1, fs2),
      codatatypes = AList.merge (op =) (op =) (cs1, cs2)})