# HG changeset patch
# User blanchet
# Date 1357119713 -3600
# Node ID e25275f7d15e3e0e04dd70c2fb473a01ea4faa88
# Parent  e0cba889369165de8b09caf8509237b51ce010d0
tuning

diff -r e0cba8893691 -r e25275f7d15e src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jan 02 09:42:57 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jan 02 10:41:53 2013 +0100
@@ -377,7 +377,7 @@
     fun learn prover =
       Sledgehammer_MaSh.mash_learn_proof ctxt params prover (prop_of goal) all_facts
   in
-    Sledgehammer_Minimize.get_minimizing_prover ctxt Sledgehammer_Provers.Normal
+    Sledgehammer_Minimize.get_minimizing_isar_prover ctxt Sledgehammer_Provers.Normal
       learn name
   end
 
diff -r e0cba8893691 -r e25275f7d15e src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Jan 02 09:42:57 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Jan 02 10:41:53 2013 +0100
@@ -525,8 +525,8 @@
        facts = facts |> map (apfst (apfst (fn name => name ())))
                      |> map Untranslated_Fact}
   in
-    get_minimizing_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
-                          problem
+    get_minimizing_isar_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
+                               problem
   end
 
 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
diff -r e0cba8893691 -r e25275f7d15e src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jan 02 09:42:57 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jan 02 10:41:53 2013 +0100
@@ -21,7 +21,7 @@
     -> Proof.state -> ((string * stature) * thm list) list
     -> ((string * stature) * thm list) list option
        * ((unit -> play) * (play -> string) * string)
-  val get_minimizing_prover :
+  val get_minimizing_isar_prover :
     Proof.context -> mode -> (string -> thm list -> unit) -> string -> prover
   val run_minimize :
     params -> (string -> thm list -> unit) -> int
@@ -325,10 +325,14 @@
       | NONE => result
     end
 
-fun get_minimizing_prover ctxt mode do_learn name params minimize_command
-                          problem =
+(* TODO: implement *)
+fun maybe_regenerate_isar_proof result = result
+
+fun get_minimizing_isar_prover ctxt mode do_learn name params minimize_command
+                               problem =
   get_prover ctxt mode name params minimize_command problem
   |> maybe_minimize ctxt mode do_learn name params problem
+  |> maybe_regenerate_isar_proof
 
 fun run_minimize (params as {provers, ...}) do_learn i refs state =
   let
diff -r e0cba8893691 -r e25275f7d15e src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jan 02 09:42:57 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jan 02 10:41:53 2013 +0100
@@ -95,7 +95,7 @@
       |> Output.urgent_message
     fun really_go () =
       problem
-      |> get_minimizing_prover ctxt mode learn name params minimize_command
+      |> get_minimizing_isar_prover ctxt mode learn name params minimize_command
       |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, ...} =>
                            print_used_facts used_facts
                          | _ => ())