# HG changeset patch
# User haftmann
# Date 1292919577 -3600
# Node ID 692c3fbde3c9bced8af31629fcd6ccae55ec0d9e
# Parent  064133cb4ef660cd7364349d8d4bc54b55e269a5
tuned naming

diff -r 064133cb4ef6 -r 692c3fbde3c9 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Tue Dec 21 09:18:29 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML	Tue Dec 21 09:19:37 2010 +0100
@@ -163,10 +163,10 @@
 
 val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (Binding.name "holds_by_evaluation",
-  fn (serializer, naming, thy, program, vs_t, deps, ct) => check_holds serializer naming thy program vs_t deps ct)));
+  fn (some_target, naming, thy, program, vs_t, deps, ct) => check_holds some_target naming thy program vs_t deps ct)));
 
-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);
+fun check_holds_oracle some_target naming thy program ((_, vs_ty), t) deps ct =
+  raw_check_holds_oracle (some_target, naming, thy, program, (vs_ty, t), deps, ct);
 
 fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
     (fn naming => check_holds_oracle NONE naming thy)