--- a/src/Tools/Code/code_simp.ML Fri Dec 17 18:24:44 2010 +0100
+++ b/src/Tools/Code/code_simp.ML Fri Dec 17 18:24:44 2010 +0100
@@ -7,7 +7,7 @@
signature CODE_SIMP =
sig
val map_ss: (simpset -> simpset) -> theory -> theory
- val dynamic_conv: conv
+ val dynamic_conv: theory -> conv
val dynamic_tac: theory -> int -> tactic
val dynamic_value: theory -> term -> term
val static_conv: theory -> simpset option -> string list -> conv
@@ -51,12 +51,12 @@
(* evaluation with dynamic code context *)
-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_conv thy = Code_Thingol.dynamic_conv thy
+ (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program);
-fun dynamic_tac thy = CONVERSION dynamic_conv THEN' conclude_tac thy NONE;
+fun dynamic_tac thy = CONVERSION (dynamic_conv thy) 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;
+fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy;
val setup = Method.setup (Binding.name "code_simp")
(Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o ProofContext.theory_of)))