tuned naming
authorhaftmann
Tue Dec 21 09:19:37 2010 +0100 (2010-12-21)
changeset 41348692c3fbde3c9
parent 41347 064133cb4ef6
child 41349 0e2a3f22f018
tuned naming
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Tue Dec 21 09:18:29 2010 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Dec 21 09:19:37 2010 +0100
     1.3 @@ -163,10 +163,10 @@
     1.4  
     1.5  val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
     1.6    (Thm.add_oracle (Binding.name "holds_by_evaluation",
     1.7 -  fn (serializer, naming, thy, program, vs_t, deps, ct) => check_holds serializer naming thy program vs_t deps ct)));
     1.8 +  fn (some_target, naming, thy, program, vs_t, deps, ct) => check_holds some_target naming thy program vs_t deps ct)));
     1.9  
    1.10 -fun check_holds_oracle serializer naming thy program ((_, vs_ty), t) deps ct =
    1.11 -  raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct);
    1.12 +fun check_holds_oracle some_target naming thy program ((_, vs_ty), t) deps ct =
    1.13 +  raw_check_holds_oracle (some_target, naming, thy, program, (vs_ty, t), deps, ct);
    1.14  
    1.15  fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
    1.16      (fn naming => check_holds_oracle NONE naming thy)