diff -r e1da70df68c1 -r c5cb19ecbd41 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Dec 17 18:24:44 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML	Fri Dec 17 18:24:44 2010 +0100
@@ -23,7 +23,7 @@
     -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a
   val static_value_exn: 'a cookie -> theory -> string option
     -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a Exn.result
-  val dynamic_holds_conv: conv
+  val dynamic_holds_conv: theory -> conv
   val static_holds_conv: theory -> string list -> conv
   val code_reflect: (string * string list option) list -> string list -> string
     -> string option -> theory -> theory
@@ -175,9 +175,9 @@
 fun check_holds_oracle serializer naming thy program ((_, vs_ty), t) deps ct =
   raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct);
 
-val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_conv thy
-  (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy)
-  o reject_vars thy);
+fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
+    (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy)
+  o reject_vars thy;
 
 fun static_holds_conv thy consts =
   let