src/Tools/Code/code_runtime.ML
changeset 65043 fd753468786f
parent 65034 1846c4551153
child 65062 dc746d43f40e
     1.1 --- a/src/Tools/Code/code_runtime.ML	Wed Feb 22 20:33:53 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Wed Feb 22 20:34:24 2017 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4    val mount_computation: Proof.context -> (string * typ) list -> typ
     1.5      -> (term -> 'ml) -> ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
     1.6    val mount_computation_conv: Proof.context -> (string * typ) list -> typ
     1.7 -    -> (term -> 'ml) -> ('ml -> conv) -> Proof.context -> conv
     1.8 +    -> (term -> 'ml) -> (Proof.context -> 'ml -> conv) -> Proof.context -> conv
     1.9    val mount_computation_check: Proof.context -> (string * typ) list
    1.10      -> (term -> truth) -> Proof.context -> conv
    1.11    val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
    1.12 @@ -435,7 +435,7 @@
    1.13        { ctxt = ctxt, consts = [] }
    1.14        (K (fn ctxt' => fn t =>
    1.15          case checked_computation cTs raw_computation ctxt' t of
    1.16 -          SOME x => conv x
    1.17 +          SOME x => conv ctxt' x
    1.18          | NONE => Conv.all_conv)));
    1.19    in fn ctxt' => preprocess ctxt' then_conv computation_conv ctxt' end;
    1.20  
    1.21 @@ -451,7 +451,7 @@
    1.22  
    1.23  fun mount_computation_check ctxt cTs raw_computation =
    1.24    mount_computation_conv ctxt cTs @{typ prop} raw_computation
    1.25 -    (K holds_oracle);
    1.26 +    ((K o K) holds_oracle);
    1.27  
    1.28  end;
    1.29