1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -654,7 +654,7 @@
     1.4      if null new_facts then
     1.5        if not auto then
     1.6          "Nothing to learn.\n\nHint: Try " ^ sendback relearn_isarN ^ " or " ^
     1.7 -        sendback relearn_atpN ^ "  to learn from scratch."
     1.8 +        sendback relearn_atpN ^ " to learn from scratch."
     1.9        else
    1.10          ""
    1.11      else
    1.12 @@ -722,13 +722,13 @@
    1.13        end
    1.14    end
    1.15  
    1.16 -fun mash_learn ctxt (params as {provers, ...}) fact_override chained_ths atp =
    1.17 +fun mash_learn ctxt (params as {provers, ...}) fact_override chained atp =
    1.18    let
    1.19 -    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    1.20 +    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    1.21      val ctxt = ctxt |> Config.put instantiate_inducts false
    1.22      val facts =
    1.23 -      nearly_all_facts ctxt false fact_override Symtab.empty css_table
    1.24 -                       chained_ths [] @{prop True}
    1.25 +      nearly_all_facts ctxt false fact_override Symtab.empty css chained []
    1.26 +                       @{prop True}
    1.27    in
    1.28       mash_learn_facts ctxt params (hd provers) false atp infinite_timeout facts
    1.29       |> Output.urgent_message