1.1 --- a/src/HOL/Tools/SMT2/smt2_real.ML	Thu Mar 13 13:18:14 2014 +0100
     1.2 +++ b/src/HOL/Tools/SMT2/smt2_real.ML	Thu Mar 13 13:18:14 2014 +0100
     1.3 @@ -116,6 +116,6 @@
     1.4    SMTLIB2_Interface.add_logic (10, smtlib_logic) #>
     1.5    setup_builtins #>
     1.6    Z3_New_Interface.add_mk_builtins z3_mk_builtins #>
     1.7 -  Z3_New_Proof_Tools.add_simproc real_linarith_proc))
     1.8 +  Z3_New_Replay_Util.add_simproc real_linarith_proc))
     1.9  
    1.10  end

     2.1 --- a/src/HOL/Tools/SMT2/z3_new_real.ML	Thu Mar 13 13:18:14 2014 +0100
     2.2 +++ b/src/HOL/Tools/SMT2/z3_new_real.ML	Thu Mar 13 13:18:14 2014 +0100
     2.3 @@ -27,6 +27,6 @@
     2.4  val _ = Theory.setup (Context.theory_map (
     2.5    Z3_New_Proof.add_type_parser real_type_parser #>
     2.6    Z3_New_Proof.add_term_parser real_term_parser #>
     2.7 -  Z3_New_Proof_Methods.add_arith_abstracter abstract))
     2.8 +  Z3_New_Replay_Methods.add_arith_abstracter abstract))
     2.9  
    2.10  end