# HG changeset patch
# User blanchet
# Date 1342815586 -7200
# Node ID 85a7fb65507a292220df4625dced483f6a7dc74d
# Parent  82fc8c956cdc152a9dca932ad39fa97d7be81032
learning should honor the fact override and the chained facts

diff -r 82fc8c956cdc -r 85a7fb65507a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -372,6 +372,7 @@
       end
     else if subcommand = minN then
       let
+        val ctxt = ctxt |> Config.put instantiate_inducts false
         val i = the_default 1 opt_i
         val params as {provers, ...} =
           get_params Minimize ctxt (("provers", [default_minimize_prover]) ::
@@ -403,8 +404,9 @@
                             override_params @
                             [("slice", ["false"]),
                              ("minimize", ["true"]),
-                             ("preplay_timeout", ["0"])])))
-           (subcommand = learn_atpN orelse subcommand = relearn_atpN)
+                             ("preplay_timeout", ["0"])]))
+                  fact_override (#facts (Proof.goal state))
+                  (subcommand = learn_atpN orelse subcommand = relearn_atpN))
     else if subcommand = kill_learnersN then
       kill_learners ()
     else if subcommand = running_learnersN then
diff -r 82fc8c956cdc -r 85a7fb65507a src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -63,7 +63,8 @@
   val mash_learn_facts :
     Proof.context -> params -> string -> bool -> bool -> Time.time -> fact list
     -> string
-  val mash_learn : Proof.context -> params -> bool -> unit
+  val mash_learn :
+    Proof.context -> params -> fact_override -> thm list -> bool -> unit
   val relevant_facts :
     Proof.context -> params -> string -> int -> fact_override -> term list
     -> term -> fact list -> fact list
@@ -116,14 +117,14 @@
     String.str c
   else
     (* fixed width, in case more digits follow *)
-    "$" ^ stringN_of_int 3 (Char.ord c)
+    "%" ^ stringN_of_int 3 (Char.ord c)
 
 fun unmeta_chars accum [] = String.implode (rev accum)
-  | unmeta_chars accum (#"$" :: d1 :: d2 :: d3 :: cs) =
+  | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
     (case Int.fromString (String.implode [d1, d2, d3]) of
        SOME n => unmeta_chars (Char.chr n :: accum) cs
      | NONE => "" (* error *))
-  | unmeta_chars _ (#"$" :: _) = "" (* error *)
+  | unmeta_chars _ (#"%" :: _) = "" (* error *)
   | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
 
 val escape_meta = String.translate meta_char
@@ -193,12 +194,10 @@
             |> map snd |> take max_facts
     end
 
-val thy_feature_prefix = "y_"
-
-val thy_feature_name_of = prefix thy_feature_prefix
-val const_name_of = prefix const_prefix
-val type_name_of = prefix type_const_prefix
-val class_name_of = prefix class_prefix
+val thy_feature_name_of = prefix "y"
+val const_name_of = prefix "c"
+val type_name_of = prefix "t"
+val class_name_of = prefix "s"
 
 fun is_likely_tautology_or_too_meta th =
   let
@@ -723,10 +722,13 @@
       end
   end
 
-fun mash_learn ctxt (params as {provers, ...}) atp =
+fun mash_learn ctxt (params as {provers, ...}) fact_override chained_ths atp =
   let
     val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
-    val facts = all_facts_of ctxt css_table
+    val ctxt = ctxt |> Config.put instantiate_inducts false
+    val facts =
+      nearly_all_facts ctxt false fact_override Symtab.empty css_table
+                       chained_ths [] @{prop True}
   in
      mash_learn_facts ctxt params (hd provers) false atp infinite_timeout facts
      |> Output.urgent_message