--- a/src/HOL/Sledgehammer.thy Wed Sep 29 23:26:39 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Wed Sep 29 23:30:10 2010 +0200
@@ -99,7 +99,7 @@
use "~~/src/Tools/Metis/metis.ML"
use "Tools/Sledgehammer/meson_clausify.ML"
-setup Meson_Clausifier.setup
+setup Meson_Clausify.setup
use "Tools/Sledgehammer/metis_translate.ML"
use "Tools/Sledgehammer/metis_reconstruct.ML"
--- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML Wed Sep 29 23:26:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML Wed Sep 29 23:30:10 2010 +0200
@@ -1,11 +1,11 @@
-(* Title: HOL/Tools/Sledgehammer/clausifier.ML
+(* Title: HOL/Tools/Sledgehammer/meson_clausify.ML
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
Author: Jasmin Blanchette, TU Muenchen
Transformation of axiom rules (elim/intro/etc) into CNF forms.
*)
-signature MESON_CLAUSIFIER =
+signature MESON_CLAUSIFY =
sig
val new_skolemizer : bool Config.T
val new_skolem_var_prefix : string
@@ -18,7 +18,7 @@
val setup: theory -> theory
end;
-structure Meson_Clausifier : MESON_CLAUSIFIER =
+structure Meson_Clausify : MESON_CLAUSIFY =
struct
val (new_skolemizer, new_skolemizer_setup) =
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Sep 29 23:26:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Sep 29 23:30:10 2010 +0200
@@ -148,7 +148,7 @@
let val thy = ProofContext.theory_of ctxt
val type_lits = Config.get ctxt type_lits
val th_cls_pairs =
- map (fn th => (Thm.get_name_hint th, Meson_Clausifier.cnf_axiom thy th))
+ map (fn th => (Thm.get_name_hint th, Meson_Clausify.cnf_axiom thy th))
ths0
val thss = map (snd o snd) th_cls_pairs
val dischargers = map_filter (fst o snd) th_cls_pairs
@@ -211,7 +211,7 @@
does, but also keep an unextensionalized version of "th" for backward
compatibility. *)
fun also_extensionalize_theorem th =
- let val th' = Meson_Clausifier.extensionalize_theorem th in
+ let val th' = Meson_Clausify.extensionalize_theorem th in
if Thm.eq_thm (th, th') then [th]
else th :: Meson.make_clauses_unsorted [th']
end
@@ -220,7 +220,7 @@
single
#> Meson.make_clauses_unsorted
#> maps also_extensionalize_theorem
- #> map Meson_Clausifier.introduce_combinators_in_theorem
+ #> map Meson_Clausify.introduce_combinators_in_theorem
#> Meson.finish_cnf
fun preskolem_tac ctxt st0 =
--- a/src/HOL/Tools/Sledgehammer/metis_translate.ML Wed Sep 29 23:26:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML Wed Sep 29 23:30:10 2010 +0200
@@ -425,7 +425,7 @@
let
val (tp, ts) = combtype_of T
val v' =
- if String.isPrefix Meson_Clausifier.new_skolem_var_prefix s then
+ if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
let
val tys = T |> strip_type |> swap |> op ::
val s' = new_skolem_name th_no s (length tys)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Sep 29 23:26:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Sep 29 23:30:10 2010 +0200
@@ -94,7 +94,7 @@
(0 upto length Ts - 1 ~~ Ts))
(* Removes the lambdas from an equation of the form "t = (%x. u)".
- (Cf. "extensionalize_theorem" in "Meson_Clausifier".) *)
+ (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
fun extensionalize_term t =
let
fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
@@ -141,7 +141,7 @@
t |> conceal_bounds Ts
|> Envir.eta_contract
|> cterm_of thy
- |> Meson_Clausifier.introduce_combinators_in_cterm
+ |> Meson_Clausify.introduce_combinators_in_cterm
|> prop_of |> Logic.dest_equals |> snd
|> reveal_bounds Ts
val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Sep 29 23:26:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Sep 29 23:30:10 2010 +0200
@@ -98,7 +98,7 @@
(* Converts an elim-rule into an equivalent theorem that does not have the
predicate variable. Leaves other theorems unchanged. We simply instantiate
the conclusion variable to False. (Cf. "transform_elim_theorem" in
- "Meson_Clausifier".) *)
+ "Meson_Clausify".) *)
fun transform_elim_term t =
case Logic.strip_imp_concl t of
@{const Trueprop} $ Var (z, @{typ bool}) =>