# HG changeset patch
# User blanchet
# Date 1285795810 -7200
# Node ID a1695e2169d0b27ea7ef4ebd403290572826c200
# Parent  21d556f109443ad9b0e74e1a8afeecaf13c3813b
finished renaming file and module

diff -r 21d556f10944 -r a1695e2169d0 src/HOL/Sledgehammer.thy
--- 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"
diff -r 21d556f10944 -r a1695e2169d0 src/HOL/Tools/Sledgehammer/meson_clausify.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) =
diff -r 21d556f10944 -r a1695e2169d0 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- 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 =
diff -r 21d556f10944 -r a1695e2169d0 src/HOL/Tools/Sledgehammer/metis_translate.ML
--- 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)
diff -r 21d556f10944 -r a1695e2169d0 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- 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
diff -r 21d556f10944 -r a1695e2169d0 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- 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}) =>