# HG changeset patch
# User blanchet
# Date 1394713094 -3600
# Node ID d530cc905c2f30c4de21c1d1af7b49bf0e5369f5
# Parent  8e7a9ad44e14f13cc1d16508c08b82de742d9939
adapted to ML structure renaming

diff -r 8e7a9ad44e14 -r d530cc905c2f src/HOL/Tools/SMT2/smt2_real.ML
--- 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
diff -r 8e7a9ad44e14 -r d530cc905c2f src/HOL/Tools/SMT2/z3_new_real.ML
--- 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