# HG changeset patch
# User blanchet
# Date 1297268338 -3600
# Node ID 839d1488045f1967746d536bb382fdf9324e2837
# Parent  4b09f8b9e0122e931ab3d3453b98c77a6731b3e5
renamed field

diff -r 4b09f8b9e012 -r 839d1488045f src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Feb 09 17:18:58 2011 +0100
@@ -393,7 +393,7 @@
           {state = st', goal = goal, subgoal = i,
            subgoal_count = Sledgehammer_Util.subgoal_count st,
            facts = facts |> map Sledgehammer_Provers.Untranslated_Fact,
-           smt_head = NONE}
+           smt_filter = NONE}
       in prover params (K "") problem end)) ()
       handle TimeLimit.TimeOut =>
              ({outcome = SOME ATP_Proof.TimedOut, message = "", used_facts = [],
diff -r 4b09f8b9e012 -r 839d1488045f src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML	Wed Feb 09 17:18:58 2011 +0100
@@ -49,7 +49,7 @@
     val problem =
       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
        facts = map Sledgehammer_Provers.Untranslated_Fact facts,
-       smt_head = NONE}
+       smt_filter = NONE}
   in
     (case prover params (K "") problem of
       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
diff -r 4b09f8b9e012 -r 839d1488045f src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Feb 09 17:18:58 2011 +0100
@@ -237,8 +237,7 @@
   {exec = ("Z3_HOME", "z3"),
    required_execs = [],
    arguments = fn _ => fn timeout => fn _ =>
-     "MBQI=true /p /t:" ^
-     string_of_int (to_secs 0 timeout),
+     "MBQI=true /p /t:" ^ string_of_int (to_secs 0 timeout),
    has_incomplete_mode = false,
    proof_delims = [],
    known_failures =
diff -r 4b09f8b9e012 -r 839d1488045f src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 09 17:18:58 2011 +0100
@@ -67,7 +67,7 @@
     val {goal, ...} = Proof.goal state
     val problem =
       {state = state, goal = goal, subgoal = i, subgoal_count = n,
-       facts = facts, smt_head = NONE}
+       facts = facts, smt_filter = NONE}
     val result as {outcome, used_facts, ...} = prover params (K "") problem
   in
     print silent (fn () =>
diff -r 4b09f8b9e012 -r 839d1488045f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Feb 09 17:18:58 2011 +0100
@@ -42,7 +42,7 @@
      subgoal: int,
      subgoal_count: int,
      facts: prover_fact list,
-     smt_head: (string * locality) SMT_Solver.smt_filter_data option}
+     smt_filter: (string * locality) SMT_Solver.smt_filter_data option}
 
   type prover_result =
     {outcome: failure option,
@@ -248,7 +248,7 @@
    subgoal: int,
    subgoal_count: int,
    facts: prover_fact list,
-   smt_head: (string * locality) SMT_Solver.smt_filter_data option}
+   smt_filter: (string * locality) SMT_Solver.smt_filter_data option}
 
 type prover_result =
   {outcome: failure option,
@@ -515,7 +515,7 @@
 val smt_monomorphize_limit = Unsynchronized.ref 4
 
 fun smt_filter_loop name ({debug, verbose, overlord, timeout, ...} : params)
-                    state i smt_head =
+                    state i smt_filter =
   let
     val ctxt = Proof.context_of state
     val repair_context =
@@ -555,7 +555,7 @@
         val _ =
           if debug then Output.urgent_message "Invoking SMT solver..." else ()
         val (outcome, used_facts) =
-          (case (iter_num, smt_head) of
+          (case (iter_num, smt_filter) of
              (1, SOME head) => head |> apsnd (apsnd repair_context)
            | _ => SMT_Solver.smt_filter_preprocess state facts i)
           |> SMT_Solver.smt_filter_apply iter_timeout
@@ -625,7 +625,7 @@
              #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
 
 fun run_smt_solver auto name (params as {debug, verbose, ...}) minimize_command
-        ({state, subgoal, subgoal_count, facts, smt_head, ...}
+        ({state, subgoal, subgoal_count, facts, smt_filter, ...}
          : prover_problem) =
   let
     val ctxt = Proof.context_of state
@@ -634,7 +634,7 @@
     val facts = facts ~~ (0 upto num_facts - 1)
                 |> map (smt_weighted_fact thy num_facts)
     val {outcome, used_facts, run_time_in_msecs} =
-      smt_filter_loop name params state subgoal smt_head facts
+      smt_filter_loop name params state subgoal smt_filter facts
     val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
     val outcome = outcome |> Option.map failure_from_smt_failure
     val message =
diff -r 4b09f8b9e012 -r 839d1488045f src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Feb 09 17:18:58 2011 +0100
@@ -86,7 +86,7 @@
 fun launch_prover
         (params as {debug, blocking, max_relevant, timeout, expect, ...})
         auto minimize_command only
-        {state, goal, subgoal, subgoal_count, facts, smt_head} name =
+        {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
   let
     val ctxt = Proof.context_of state
     val birth_time = Time.now ()
@@ -99,7 +99,7 @@
     val problem =
       {state = state, goal = goal, subgoal = subgoal,
        subgoal_count = subgoal_count, facts = take num_facts facts,
-       smt_head = smt_head}
+       smt_filter = smt_filter}
     fun really_go () =
       problem
       |> get_minimizing_prover ctxt auto name params (minimize_command name)
@@ -188,7 +188,7 @@
               | NONE => ()
       val _ = if auto then () else Output.urgent_message "Sledgehammering..."
       val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
-      fun launch_provers state get_facts translate maybe_smt_head provers =
+      fun launch_provers state get_facts translate maybe_smt_filter provers =
         let
           val facts = get_facts ()
           val num_facts = length facts
@@ -197,7 +197,7 @@
           val problem =
             {state = state, goal = goal, subgoal = i, subgoal_count = n,
              facts = facts,
-             smt_head = maybe_smt_head
+             smt_filter = maybe_smt_filter
                   (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
           val launch = launch_prover params auto minimize_command only
         in
@@ -253,13 +253,13 @@
           let
             val facts = get_facts "SMT solver" true smt_relevance_fudge smts
             val weight = SMT_Weighted_Fact oo weight_smt_fact thy
-            fun smt_head facts =
+            fun smt_filter facts =
               (if debug then curry (op o) SOME else try)
                   (SMT_Solver.smt_filter_preprocess state (facts ()))
           in
             smts |> map (`(class_of_smt_solver ctxt))
                  |> AList.group (op =)
-                 |> map (launch_provers state (K facts) weight smt_head o snd)
+                 |> map (launch_provers state (K facts) weight smt_filter o snd)
                  |> exists fst |> rpair state
           end
       fun launch_atps_and_smt_solvers () =