diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/z3_new_replay_methods.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -1,11 +1,11 @@
-(*  Title:      HOL/Tools/SMT2/z3_new_proof.ML
+(*  Title:      HOL/Tools/SMT2/z3_new_replay_methods.ML
     Author:     Sascha Boehme, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
 
 Proof methods for replaying Z3 proofs.
 *)
 
-signature Z3_NEW_PROOF_METHODS =
+signature Z3_NEW_REPLAY_METHODS =
 sig
   (*abstraction*)
   type abs_context = int * term Termtab.table
@@ -53,7 +53,7 @@
   val method_for: Z3_New_Proof.z3_rule -> z3_method
 end
 
-structure Z3_New_Proof_Methods: Z3_NEW_PROOF_METHODS =
+structure Z3_New_Replay_Methods: Z3_NEW_REPLAY_METHODS =
 struct
 
 type z3_method = Proof.context -> thm list -> term -> thm
@@ -90,7 +90,7 @@
 
 fun dest_thm thm = dest_prop (Thm.concl_of thm)
 
-fun certify_prop ctxt t = SMT2_Utils.certify ctxt (as_prop t)
+fun certify_prop ctxt t = SMT2_Util.certify ctxt (as_prop t)
 
 fun try_provers ctxt rule [] thms t = replay_rule_error ctxt rule thms t
   | try_provers ctxt rule ((name, prover) :: named_provers) thms t =
@@ -116,12 +116,12 @@
 
 fun match_instantiate ctxt t thm =
   let
-    val cert = SMT2_Utils.certify ctxt
+    val cert = SMT2_Util.certify ctxt
     val thm' = match_instantiateT ctxt t thm
   in Thm.instantiate ([], gen_certify_inst snd Var cert ctxt thm' t) thm' end
 
 fun apply_rule ctxt t =
-  (case Z3_New_Proof_Rules.apply ctxt (certify_prop ctxt t) of
+  (case Z3_New_Replay_Rules.apply ctxt (certify_prop ctxt t) of
     SOME thm => thm
   | NONE => raise Fail "apply_rule")