# HG changeset patch
# User haftmann
# Date 1282557092 -7200
# Node ID febcd17332291d7a6ac297b38379f1dd15fd3ea5
# Parent  3c7db0192db95e0df5c3a2817a46424a9cb44f01
use Code_Thingol.static_eval_conv_simple

diff -r 3c7db0192db9 -r febcd1733229 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Mon Aug 23 11:51:32 2010 +0200
+++ b/src/Tools/Code/code_simp.ML	Mon Aug 23 11:51:32 2010 +0200
@@ -82,8 +82,8 @@
 
 (* evaluation with freezed code context *)
 
-fun static_eval_conv thy some_ss consts = no_frees_conv (Code_Preproc.pre_post_conv thy
-  ((rewrite_modulo thy some_ss o snd o snd o Code_Thingol.consts_program thy false) consts));
+fun static_eval_conv thy some_ss consts = no_frees_conv
+  (Code_Thingol.static_eval_conv_simple thy consts (rewrite_modulo thy some_ss));
 
 fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
   THEN' conclude_tac thy some_ss;