src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 53531 2780628e9656
parent 53530 6e817f070f66
child 53532 4ad9599a0847
     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