--- a/src/HOL/Tools/SMT2/smt2_real.ML Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_real.ML Thu Mar 13 13:18:14 2014 +0100
@@ -116,6 +116,6 @@
SMTLIB2_Interface.add_logic (10, smtlib_logic) #>
setup_builtins #>
Z3_New_Interface.add_mk_builtins z3_mk_builtins #>
- Z3_New_Proof_Tools.add_simproc real_linarith_proc))
+ Z3_New_Replay_Util.add_simproc real_linarith_proc))
end
--- a/src/HOL/Tools/SMT2/z3_new_real.ML Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_real.ML Thu Mar 13 13:18:14 2014 +0100
@@ -27,6 +27,6 @@
val _ = Theory.setup (Context.theory_map (
Z3_New_Proof.add_type_parser real_type_parser #>
Z3_New_Proof.add_term_parser real_term_parser #>
- Z3_New_Proof_Methods.add_arith_abstracter abstract))
+ Z3_New_Replay_Methods.add_arith_abstracter abstract))
end