1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Sep 11 14:07:24 2013 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Sep 11 14:07:24 2013 +0200
1.3 @@ -187,7 +187,7 @@
1.4 "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
1.5 "weak_case_cong", "nat_of_char_simps", "nibble.simps",
1.6 "nibble.distinct"]
1.7 - |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
1.8 + |> not (ho_atp orelse Config.get ctxt instantiate_inducts) ?
1.9 append ["induct", "inducts"]
1.10 |> map (prefix Long_Name.separator)
1.11