remove spurious parameter to "merge"
authorblanchet
Tue, 10 Nov 2009 14:20:15 +0100
changeset 33584 488837bf01d7
parent 33583 b5e0909cd5ea
child 33592 27f74e853a54
remove spurious parameter to "merge"
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 *)