# HG changeset patch
# User blanchet
# Date 1416389475 -3600
# Node ID cc5e345753541c91b6859b3f035cc637f4fb3a02
# Parent  f319054e8dffd908d220e7058a82900b08d89c70
tuning

diff -r f319054e8dff -r cc5e34575354 src/HOL/Tools/SMT/verit_proof.ML
--- a/src/HOL/Tools/SMT/verit_proof.ML	Wed Nov 19 10:31:15 2014 +0100
+++ b/src/HOL/Tools/SMT/verit_proof.ML	Wed Nov 19 10:31:15 2014 +0100
@@ -54,11 +54,11 @@
   VeriT_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes}
 
 val veriT_step_prefix = ".c"
-val veriT_alpha_conv_rule = "tmp_alphaconv"
 val veriT_input_rule = "input"
 val veriT_la_generic_rule = "la_generic"
 val veriT_rewrite_rule = "__rewrite" (* arbitrary *)
 val veriT_simp_arith_rule = "simp_arith"
+val veriT_tmp_alphaconv_rule = "tmp_alphaconv"
 val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
 val veriT_tmp_skolemize_rule = "tmp_skolemize"
 
@@ -293,7 +293,7 @@
       val correct_dependency = map (perhaps (Symtab.lookup replace_table))
       val find_predecessor = perhaps (Symtab.lookup replace_table)
     in
-      if rule = veriT_alpha_conv_rule then
+      if rule = veriT_tmp_alphaconv_rule then
         remove_alpha_conversion (Symtab.update (id, find_predecessor (hd prems))
           replace_table) steps
       else