# HG changeset patch
# User haftmann
# Date 1292488099 -3600
# Node ID 7cded8957e72f7ec0ebcc66d30a95ba62b3b83f0
# Parent  b0b975e197b5e72f3e7d075db9c4163366e8468e
more uniform naming

diff -r b0b975e197b5 -r 7cded8957e72 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Thu Dec 16 09:26:46 2010 +0100
+++ b/src/Tools/Code/code_simp.ML	Thu Dec 16 09:28:19 2010 +0100
@@ -8,10 +8,10 @@
 sig
   val map_ss: (simpset -> simpset) -> theory -> theory
   val dynamic_conv: conv
-  val dynamic_eval_tac: theory -> int -> tactic
+  val dynamic_tac: theory -> int -> tactic
   val dynamic_value: theory -> term -> term
   val static_conv: theory -> simpset option -> string list -> conv
-  val static_eval_tac: theory -> simpset option -> string list -> int -> tactic
+  val static_tac: theory -> simpset option -> string list -> int -> tactic
   val setup: theory -> theory
 end;
 
@@ -54,12 +54,12 @@
 val dynamic_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_conv thy
   (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
 
-fun dynamic_eval_tac thy = CONVERSION dynamic_conv THEN' conclude_tac thy NONE;
+fun dynamic_tac thy = CONVERSION dynamic_conv THEN' conclude_tac thy NONE;
 
 fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv o Thm.cterm_of thy;
 
 val setup = Method.setup (Binding.name "code_simp")
-  (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_eval_tac o ProofContext.theory_of)))
+  (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o ProofContext.theory_of)))
   "simplification with code equations"
   #> Value.add_evaluator ("simp", dynamic_value o ProofContext.theory_of);
 
@@ -70,7 +70,7 @@
   Code_Thingol.static_conv_simple thy consts
     (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program);
 
-fun static_eval_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts)
+fun static_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts)
   THEN' conclude_tac thy some_ss;
 
 end;