# HG changeset patch
# User blanchet
# Date 1283151207 -7200
# Node ID fd803530e8a0a399dacde2799cb426d48e33d20d
# Parent  d0e3f68dde632f96c03fc3b6b1c0b77eef717234
bring Sledgehammer's combinators in line with Metis's;
cf. email from Larry

diff -r d0e3f68dde63 -r fd803530e8a0 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 27 18:04:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Aug 30 08:53:27 2010 +0200
@@ -218,8 +218,10 @@
   count_combformula combformula
 
 val optional_helpers =
-  [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
-   (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
+  [(["c_COMBI"], @{thms COMBI_def}),
+   (["c_COMBK"], @{thms COMBK_def}),
+   (["c_COMBB"], @{thms COMBB_def}),
+   (["c_COMBC"], @{thms COMBC_def}),
    (["c_COMBS"], @{thms COMBS_def})]
 val optional_typed_helpers =
   [(["c_True", "c_False", "c_If"], @{thms True_or_False}),