# HG changeset patch
# User blanchet
# Date 1378901244 -7200
# Node ID 2780628e965687814a05ff5965f7354af84fbbb1
# Parent  6e817f070f66e4c854ffb99e529fc20c4d6cd1e0
tuning

diff -r 6e817f070f66 -r 2780628e9656 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Sep 11 14:07:24 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Sep 11 14:07:24 2013 +0200
@@ -187,7 +187,7 @@
    "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
    "weak_case_cong", "nat_of_char_simps", "nibble.simps",
    "nibble.distinct"]
-  |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
+  |> not (ho_atp orelse Config.get ctxt instantiate_inducts) ?
         append ["induct", "inducts"]
   |> map (prefix Long_Name.separator)