1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -372,6 +372,7 @@
     1.4        end
     1.5      else if subcommand = minN then
     1.6        let
     1.7 +        val ctxt = ctxt |> Config.put instantiate_inducts false
     1.8          val i = the_default 1 opt_i
     1.9          val params as {provers, ...} =
    1.10            get_params Minimize ctxt (("provers", [default_minimize_prover]) ::
    1.11 @@ -403,8 +404,9 @@
    1.12                              override_params @
    1.13                              [("slice", ["false"]),
    1.14                               ("minimize", ["true"]),
    1.15 -                             ("preplay_timeout", ["0"])])))
    1.16 -           (subcommand = learn_atpN orelse subcommand = relearn_atpN)
    1.17 +                             ("preplay_timeout", ["0"])]))
    1.18 +                  fact_override (#facts (Proof.goal state))
    1.19 +                  (subcommand = learn_atpN orelse subcommand = relearn_atpN))
    1.20      else if subcommand = kill_learnersN then
    1.21        kill_learners ()
    1.22      else if subcommand = running_learnersN then

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     2.3 @@ -63,7 +63,8 @@
     2.4    val mash_learn_facts :
     2.5      Proof.context -> params -> string -> bool -> bool -> Time.time -> fact list
     2.6      -> string
     2.7 -  val mash_learn : Proof.context -> params -> bool -> unit
     2.8 +  val mash_learn :
     2.9 +    Proof.context -> params -> fact_override -> thm list -> bool -> unit
    2.10    val relevant_facts :
    2.11      Proof.context -> params -> string -> int -> fact_override -> term list
    2.12      -> term -> fact list -> fact list
    2.13 @@ -116,14 +117,14 @@
    2.14      String.str c
    2.15    else
    2.16      (* fixed width, in case more digits follow *)
    2.17 -    "$" ^ stringN_of_int 3 (Char.ord c)
    2.18 +    "%" ^ stringN_of_int 3 (Char.ord c)
    2.19  
    2.20  fun unmeta_chars accum [] = String.implode (rev accum)
    2.21 -  | unmeta_chars accum (#"$" :: d1 :: d2 :: d3 :: cs) =
    2.22 +  | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
    2.23      (case Int.fromString (String.implode [d1, d2, d3]) of
    2.24         SOME n => unmeta_chars (Char.chr n :: accum) cs
    2.25       | NONE => "" (* error *))
    2.26 -  | unmeta_chars _ (#"$" :: _) = "" (* error *)
    2.27 +  | unmeta_chars _ (#"%" :: _) = "" (* error *)
    2.28    | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
    2.29  
    2.30  val escape_meta = String.translate meta_char
    2.31 @@ -193,12 +194,10 @@
    2.32              |> map snd |> take max_facts
    2.33      end
    2.34  
    2.35 -val thy_feature_prefix = "y_"
    2.36 -
    2.37 -val thy_feature_name_of = prefix thy_feature_prefix
    2.38 -val const_name_of = prefix const_prefix
    2.39 -val type_name_of = prefix type_const_prefix
    2.40 -val class_name_of = prefix class_prefix
    2.41 +val thy_feature_name_of = prefix "y"
    2.42 +val const_name_of = prefix "c"
    2.43 +val type_name_of = prefix "t"
    2.44 +val class_name_of = prefix "s"
    2.45  
    2.46  fun is_likely_tautology_or_too_meta th =
    2.47    let
    2.48 @@ -723,10 +722,13 @@
    2.49        end
    2.50    end
    2.51  
    2.52 -fun mash_learn ctxt (params as {provers, ...}) atp =
    2.53 +fun mash_learn ctxt (params as {provers, ...}) fact_override chained_ths atp =
    2.54    let
    2.55      val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    2.56 -    val facts = all_facts_of ctxt css_table
    2.57 +    val ctxt = ctxt |> Config.put instantiate_inducts false
    2.58 +    val facts =
    2.59 +      nearly_all_facts ctxt false fact_override Symtab.empty css_table
    2.60 +                       chained_ths [] @{prop True}
    2.61    in
    2.62       mash_learn_facts ctxt params (hd provers) false atp infinite_timeout facts
    2.63       |> Output.urgent_message