# HG changeset patch
# User blanchet
# Date 1283291459 -7200
# Node ID 483879af0643b33f47bb8c0813cd5e77f36900ea
# Parent  96fae8916d8b02d63f94e39792390415017e06f7
finished renaming

diff -r 96fae8916d8b -r 483879af0643 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 31 23:50:59 2010 +0200
@@ -290,7 +290,7 @@
     | NONE => get_prover (default_atp_name ()))
   end
 
-type locality = Sledgehammer_Fact_Filter.locality
+type locality = Sledgehammer_Filter.locality
 
 local
 
@@ -357,7 +357,7 @@
     case result of
       SH_OK (time_isa, time_atp, names) =>
         let
-          fun get_thms (name, Sledgehammer_Fact_Filter.Chained) = NONE
+          fun get_thms (name, Sledgehammer_Filter.Chained) = NONE
             | get_thms (name, loc) =
               SOME ((name, loc), thms_of_name (Proof.context_of st) name)
         in
@@ -396,7 +396,7 @@
     val params = Sledgehammer_Isar.default_params thy
       [("atps", prover_name), ("timeout", Int.toString timeout ^ " s")]
     val minimize =
-      Sledgehammer_Fact_Minimize.minimize_theorems params 1 (subgoal_count st)
+      Sledgehammer_Minimize.minimize_theorems params 1 (subgoal_count st)
     val _ = log separator
   in
     case minimize st (these (!named_thms)) of
diff -r 96fae8916d8b -r 483879af0643 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue Aug 31 23:50:59 2010 +0200
@@ -6,21 +6,20 @@
 struct
 
 val relevance_filter_args =
-  [("worse_irrel_freq", Sledgehammer_Fact_Filter.worse_irrel_freq),
-   ("higher_order_irrel_weight",
-    Sledgehammer_Fact_Filter.higher_order_irrel_weight),
-   ("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight),
-   ("abs_irrel_weight", Sledgehammer_Fact_Filter.abs_irrel_weight),
-   ("skolem_irrel_weight", Sledgehammer_Fact_Filter.skolem_irrel_weight),
-   ("intro_bonus", Sledgehammer_Fact_Filter.intro_bonus),
-   ("elim_bonus", Sledgehammer_Fact_Filter.elim_bonus),
-   ("simp_bonus", Sledgehammer_Fact_Filter.simp_bonus),
-   ("local_bonus", Sledgehammer_Fact_Filter.local_bonus),
-   ("chained_bonus", Sledgehammer_Fact_Filter.chained_bonus),
-   ("max_imperfect", Sledgehammer_Fact_Filter.max_imperfect),
-   ("max_imperfect_exp", Sledgehammer_Fact_Filter.max_imperfect_exp),
-   ("threshold_divisor", Sledgehammer_Fact_Filter.threshold_divisor),
-   ("ridiculous_threshold", Sledgehammer_Fact_Filter.ridiculous_threshold)]
+  [("worse_irrel_freq", Sledgehammer_Filter.worse_irrel_freq),
+   ("higher_order_irrel_weight", Sledgehammer_Filter.higher_order_irrel_weight),
+   ("abs_rel_weight", Sledgehammer_Filter.abs_rel_weight),
+   ("abs_irrel_weight", Sledgehammer_Filter.abs_irrel_weight),
+   ("skolem_irrel_weight", Sledgehammer_Filter.skolem_irrel_weight),
+   ("intro_bonus", Sledgehammer_Filter.intro_bonus),
+   ("elim_bonus", Sledgehammer_Filter.elim_bonus),
+   ("simp_bonus", Sledgehammer_Filter.simp_bonus),
+   ("local_bonus", Sledgehammer_Filter.local_bonus),
+   ("chained_bonus", Sledgehammer_Filter.chained_bonus),
+   ("max_imperfect", Sledgehammer_Filter.max_imperfect),
+   ("max_imperfect_exp", Sledgehammer_Filter.max_imperfect_exp),
+   ("threshold_divisor", Sledgehammer_Filter.threshold_divisor),
+   ("ridiculous_threshold", Sledgehammer_Filter.ridiculous_threshold)]
 
 structure Prooftab =
   Table(type key = int * int val ord = prod_ord int_ord int_ord);
@@ -104,7 +103,7 @@
          val subgoal = 1
          val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
          val facts =
-           Sledgehammer_Fact_Filter.relevant_facts ctxt full_types
+           Sledgehammer_Filter.relevant_facts ctxt full_types
                relevance_thresholds
                (the_default default_max_relevant max_relevant)
                (the_default false theory_relevant)
diff -r 96fae8916d8b -r 483879af0643 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Tue Aug 31 23:50:59 2010 +0200
@@ -19,11 +19,11 @@
   ("Tools/Sledgehammer/metis_clauses.ML")
   ("Tools/Sledgehammer/metis_tactics.ML")
   ("Tools/Sledgehammer/sledgehammer_util.ML")
-  ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
+  ("Tools/Sledgehammer/sledgehammer_filter.ML")
   ("Tools/Sledgehammer/sledgehammer_translate.ML")
-  ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
+  ("Tools/Sledgehammer/sledgehammer_reconstruct.ML")
   ("Tools/Sledgehammer/sledgehammer.ML")
-  ("Tools/Sledgehammer/sledgehammer_fact_minimize.ML")
+  ("Tools/Sledgehammer/sledgehammer_minimize.ML")
   ("Tools/Sledgehammer/sledgehammer_isar.ML")
 begin
 
@@ -103,12 +103,12 @@
 use "Tools/Sledgehammer/metis_tactics.ML"
 
 use "Tools/Sledgehammer/sledgehammer_util.ML"
-use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
+use "Tools/Sledgehammer/sledgehammer_filter.ML"
 use "Tools/Sledgehammer/sledgehammer_translate.ML"
-use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
+use "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
 use "Tools/Sledgehammer/sledgehammer.ML"
 setup Sledgehammer.setup
-use "Tools/Sledgehammer/sledgehammer_fact_minimize.ML"
+use "Tools/Sledgehammer/sledgehammer_minimize.ML"
 use "Tools/Sledgehammer/sledgehammer_isar.ML"
 setup Metis_Tactics.setup
 
diff -r 96fae8916d8b -r 483879af0643 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Aug 31 23:50:59 2010 +0200
@@ -9,9 +9,9 @@
 signature SLEDGEHAMMER =
 sig
   type failure = ATP_Systems.failure
-  type locality = Sledgehammer_Fact_Filter.locality
-  type relevance_override = Sledgehammer_Fact_Filter.relevance_override
-  type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
+  type locality = Sledgehammer_Filter.locality
+  type relevance_override = Sledgehammer_Filter.relevance_override
+  type minimize_command = Sledgehammer_Reconstruct.minimize_command
   type params =
     {blocking: bool,
      debug: bool,
@@ -64,9 +64,9 @@
 open ATP_Systems
 open Metis_Clauses
 open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
+open Sledgehammer_Filter
 open Sledgehammer_Translate
-open Sledgehammer_Proof_Reconstruct
+open Sledgehammer_Reconstruct
 
 
 (** The Sledgehammer **)
@@ -179,7 +179,7 @@
   #> snd #> Substring.string #> strip_spaces_except_between_ident_chars
   #> explode #> parse_clause_formula_relation #> fst
 
-(* TODO: move to "Sledgehammer_Proof_Reconstruct.ML" *)
+(* TODO: move to "Sledgehammer_Reconstruct" *)
 fun repair_conjecture_shape_and_theorem_names output conjecture_shape
                                               axiom_names =
   if String.isSubstring set_ClauseFormulaRelationN output then
diff -r 96fae8916d8b -r 483879af0643 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Aug 31 23:50:59 2010 +0200
@@ -1,9 +1,9 @@
-(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_filter.ML
     Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     Author:     Jasmin Blanchette, TU Muenchen
 *)
 
-signature SLEDGEHAMMER_FACT_FILTER =
+signature SLEDGEHAMMER_FILTER =
 sig
   datatype locality = General | Intro | Elim | Simp | Local | Chained
 
@@ -35,7 +35,7 @@
     -> thm list -> term list -> term -> ((string * locality) * thm) list
 end;
 
-structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
+structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
 struct
 
 open Sledgehammer_Util
diff -r 96fae8916d8b -r 483879af0643 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 31 23:50:59 2010 +0200
@@ -20,7 +20,7 @@
 open ATP_Systems
 open Sledgehammer_Util
 open Sledgehammer
-open Sledgehammer_Fact_Minimize
+open Sledgehammer_Minimize
 
 (** Sledgehammer commands **)
 
diff -r 96fae8916d8b -r 483879af0643 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Aug 31 23:50:59 2010 +0200
@@ -1,13 +1,13 @@
-(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
     Author:     Philipp Meyer, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
 
 Minimization of theorem list for Metis using automatic theorem provers.
 *)
 
-signature SLEDGEHAMMER_FACT_MINIMIZE =
+signature SLEDGEHAMMER_MINIMIZE =
 sig
-  type locality = Sledgehammer_Fact_Filter.locality
+  type locality = Sledgehammer_Filter.locality
   type params = Sledgehammer.params
 
   val minimize_theorems :
@@ -16,13 +16,13 @@
   val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
 end;
 
-structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE =
+structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
 struct
 
 open ATP_Systems
 open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
-open Sledgehammer_Proof_Reconstruct
+open Sledgehammer_Filter
+open Sledgehammer_Reconstruct
 open Sledgehammer
 
 (* wrapper for calling external prover *)
diff -r 96fae8916d8b -r 483879af0643 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Aug 31 23:50:59 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     Author:     Claire Quigley, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
@@ -6,9 +6,9 @@
 Transfer of proofs from external provers.
 *)
 
-signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
+signature SLEDGEHAMMER_RECONSTRUCT =
 sig
-  type locality = Sledgehammer_Fact_Filter.locality
+  type locality = Sledgehammer_Filter.locality
   type minimize_command = string list -> string
   type metis_params =
     bool * minimize_command * string * (string * locality) list vector * thm
@@ -22,13 +22,13 @@
   val proof_text : bool -> isar_params -> metis_params -> text_result
 end;
 
-structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
+structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
 struct
 
 open ATP_Problem
 open Metis_Clauses
 open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
+open Sledgehammer_Filter
 open Sledgehammer_Translate
 
 type minimize_command = string list -> string