1.1 --- a/src/Tools/Code/code_simp.ML	Thu Jun 17 10:02:29 2010 +0200
     1.2 +++ b/src/Tools/Code/code_simp.ML	Thu Jun 17 10:45:10 2010 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    val map_ss: (simpset -> simpset) -> theory -> theory
     1.5    val current_conv: theory -> conv
     1.6    val current_tac: theory -> int -> tactic
     1.7 +  val current_value: theory -> term -> term
     1.8    val make_conv: theory -> simpset option -> string list -> conv
     1.9    val make_tac: theory -> simpset option -> string list -> int -> tactic
    1.10    val setup: theory -> theory
    1.11 @@ -68,9 +69,12 @@
    1.12  
    1.13  fun current_tac thy = CONVERSION (current_conv thy);
    1.14  
    1.15 +fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy
    1.16 +
    1.17  val setup = Method.setup (Binding.name "code_simp")
    1.18    (Scan.succeed (SIMPLE_METHOD' o current_tac o ProofContext.theory_of))
    1.19    "simplification with code equations"
    1.20 +  #> Value.add_evaluator ("simp", current_value o ProofContext.theory_of);
    1.21  
    1.22  
    1.23  (* evaluation with freezed code context *)