1.1 --- a/src/Tools/Code/code_simp.ML	Thu Dec 16 09:26:46 2010 +0100
     1.2 +++ b/src/Tools/Code/code_simp.ML	Thu Dec 16 09:28:19 2010 +0100
     1.3 @@ -8,10 +8,10 @@
     1.4  sig
     1.5    val map_ss: (simpset -> simpset) -> theory -> theory
     1.6    val dynamic_conv: conv
     1.7 -  val dynamic_eval_tac: theory -> int -> tactic
     1.8 +  val dynamic_tac: theory -> int -> tactic
     1.9    val dynamic_value: theory -> term -> term
    1.10    val static_conv: theory -> simpset option -> string list -> conv
    1.11 -  val static_eval_tac: theory -> simpset option -> string list -> int -> tactic
    1.12 +  val static_tac: theory -> simpset option -> string list -> int -> tactic
    1.13    val setup: theory -> theory
    1.14  end;
    1.15  
    1.16 @@ -54,12 +54,12 @@
    1.17  val dynamic_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_conv thy
    1.18    (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
    1.19  
    1.20 -fun dynamic_eval_tac thy = CONVERSION dynamic_conv THEN' conclude_tac thy NONE;
    1.21 +fun dynamic_tac thy = CONVERSION dynamic_conv THEN' conclude_tac thy NONE;
    1.22  
    1.23  fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv o Thm.cterm_of thy;
    1.24  
    1.25  val setup = Method.setup (Binding.name "code_simp")
    1.26 -  (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_eval_tac o ProofContext.theory_of)))
    1.27 +  (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o ProofContext.theory_of)))
    1.28    "simplification with code equations"
    1.29    #> Value.add_evaluator ("simp", dynamic_value o ProofContext.theory_of);
    1.30  
    1.31 @@ -70,7 +70,7 @@
    1.32    Code_Thingol.static_conv_simple thy consts
    1.33      (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program);
    1.34  
    1.35 -fun static_eval_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts)
    1.36 +fun static_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts)
    1.37    THEN' conclude_tac thy some_ss;
    1.38  
    1.39  end;