# HG changeset patch
# User wenzelm
# Date 1257883338 -3600
# Node ID 89c43964696068196e440fd5480e0cb46a5901ec
# Parent  d7784ad2680de0b95618ff7d832766164e1a8e4f
recovered update from 7264824baf66, which got lost in 7264824baf66;

diff -r d7784ad2680d -r 89c439646960 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Nov 10 18:32:41 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Nov 10 21:02:18 2009 +0100
@@ -135,9 +135,8 @@
 structure Data = Theory_Data(
   type T = {params: raw_param list}
   val empty = {params = rev default_default_params}
-  val copy = I
   val extend = I
-  fun merge ({params = ps1}, {params = ps2}) =
+  fun merge ({params = ps1}, {params = ps2}) : T =
     {params = AList.merge (op =) (op =) (ps1, ps2)})
 
 (* raw_param -> theory -> theory *)