# HG changeset patch
# User blanchet
# Date 1257859215 -3600
# Node ID 488837bf01d7eb605a4d100bd2611617d659515e
# Parent  b5e0909cd5eaca1c37bbd0cad12fee19aa6a42e8
remove spurious parameter to "merge"

diff -r b5e0909cd5ea -r 488837bf01d7 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Nov 10 13:54:00 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Nov 10 14:20:15 2009 +0100
@@ -137,7 +137,7 @@
   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}) =
     {params = AList.merge (op =) (op =) (ps1, ps2)})
 
 (* raw_param -> theory -> theory *)