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 @@ -63,7 +63,8 @@
     1.4    val mash_learn_facts :
     1.5      Proof.context -> params -> string -> bool -> bool -> Time.time -> fact list
     1.6      -> string
     1.7 -  val mash_learn : Proof.context -> params -> bool -> unit
     1.8 +  val mash_learn :
     1.9 +    Proof.context -> params -> fact_override -> thm list -> bool -> unit
    1.10    val relevant_facts :
    1.11      Proof.context -> params -> string -> int -> fact_override -> term list
    1.12      -> term -> fact list -> fact list
    1.13 @@ -116,14 +117,14 @@
    1.14      String.str c
    1.15    else
    1.16      (* fixed width, in case more digits follow *)
    1.17 -    "$" ^ stringN_of_int 3 (Char.ord c)
    1.18 +    "%" ^ stringN_of_int 3 (Char.ord c)
    1.19  
    1.20  fun unmeta_chars accum [] = String.implode (rev accum)
    1.21 -  | unmeta_chars accum (#"$" :: d1 :: d2 :: d3 :: cs) =
    1.22 +  | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
    1.23      (case Int.fromString (String.implode [d1, d2, d3]) of
    1.24         SOME n => unmeta_chars (Char.chr n :: accum) cs
    1.25       | NONE => "" (* error *))
    1.26 -  | unmeta_chars _ (#"$" :: _) = "" (* error *)
    1.27 +  | unmeta_chars _ (#"%" :: _) = "" (* error *)
    1.28    | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
    1.29  
    1.30  val escape_meta = String.translate meta_char
    1.31 @@ -193,12 +194,10 @@
    1.32              |> map snd |> take max_facts
    1.33      end
    1.34  
    1.35 -val thy_feature_prefix = "y_"
    1.36 -
    1.37 -val thy_feature_name_of = prefix thy_feature_prefix
    1.38 -val const_name_of = prefix const_prefix
    1.39 -val type_name_of = prefix type_const_prefix
    1.40 -val class_name_of = prefix class_prefix
    1.41 +val thy_feature_name_of = prefix "y"
    1.42 +val const_name_of = prefix "c"
    1.43 +val type_name_of = prefix "t"
    1.44 +val class_name_of = prefix "s"
    1.45  
    1.46  fun is_likely_tautology_or_too_meta th =
    1.47    let
    1.48 @@ -723,10 +722,13 @@
    1.49        end
    1.50    end
    1.51  
    1.52 -fun mash_learn ctxt (params as {provers, ...}) atp =
    1.53 +fun mash_learn ctxt (params as {provers, ...}) fact_override chained_ths atp =
    1.54    let
    1.55      val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    1.56 -    val facts = all_facts_of ctxt css_table
    1.57 +    val ctxt = ctxt |> Config.put instantiate_inducts false
    1.58 +    val facts =
    1.59 +      nearly_all_facts ctxt false fact_override Symtab.empty css_table
    1.60 +                       chained_ths [] @{prop True}
    1.61    in
    1.62       mash_learn_facts ctxt params (hd provers) false atp infinite_timeout facts
    1.63       |> Output.urgent_message