--- a/src/Doc/Codegen/Computations.thy Wed Feb 22 20:33:53 2017 +0100
+++ b/src/Doc/Codegen/Computations.thy Wed Feb 22 20:34:24 2017 +0100
@@ -286,7 +286,7 @@
"minus :: int \<Rightarrow> int \<Rightarrow> int"
"times :: int \<Rightarrow> int \<Rightarrow> int"
"0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int"
- } (curry dvd_oracle)
+ } (K (curry dvd_oracle))
end
\<close>
@@ -345,15 +345,15 @@
val divisor = Thm.dest_arg o Thm.dest_arg;
- fun evaluate thm =
- Simplifier.rewrite_rule
- (Proof_Context.transfer (Thm.theory_of_thm thm) @{context})
- (map mk_eq @{thms arith_simps positive_mult}) thm; (*FIXME proper ctxt*)
+ val evaluate_simps = map mk_eq @{thms arith_simps positive_mult};
- fun revaluate k ct =
+ fun evaluate ctxt =
+ Simplifier.rewrite_rule ctxt evaluate_simps;
+
+ fun revaluate ctxt k ct =
@{thm conv_div_cert}
|> Thm.instantiate' [] [SOME (cterm_of_int k), SOME (divisor ct)]
- |> evaluate;
+ |> evaluate ctxt;
in
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Wed Feb 22 20:33:53 2017 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Wed Feb 22 20:34:24 2017 +0100
@@ -682,7 +682,7 @@
"0::nat" "1::nat" "2::nat" "3::nat"
"0::int" "1::int" "2::int" "3::int" "-1::int"
datatypes: polex "(polex * polex) list" int integer num}
- (fn p => fn ct => pol_oracle @{context} ct (term_of_pol p))
+ (fn ctxt => fn p => fn ct => pol_oracle ctxt ct (term_of_pol p))
end
\<close>
--- a/src/HOL/Decision_Procs/Reflective_Field.thy Wed Feb 22 20:33:53 2017 +0100
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy Wed Feb 22 20:34:24 2017 +0100
@@ -675,7 +675,7 @@
"0::nat" "1::nat" "2::nat" "3::nat"
"0::int" "1::int" "2::int" "3::int" "-1::int"
datatypes: fexpr int integer num}
- (fn result => fn ct => fnorm_oracle @{context} ct (term_of_result result))
+ (fn ctxt => fn result => fn ct => fnorm_oracle ctxt ct (term_of_result result))
end
\<close>
--- a/src/Tools/Code/code_runtime.ML Wed Feb 22 20:33:53 2017 +0100
+++ b/src/Tools/Code/code_runtime.ML Wed Feb 22 20:34:24 2017 +0100
@@ -35,7 +35,7 @@
val mount_computation: Proof.context -> (string * typ) list -> typ
-> (term -> 'ml) -> ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
val mount_computation_conv: Proof.context -> (string * typ) list -> typ
- -> (term -> 'ml) -> ('ml -> conv) -> Proof.context -> conv
+ -> (term -> 'ml) -> (Proof.context -> 'ml -> conv) -> Proof.context -> conv
val mount_computation_check: Proof.context -> (string * typ) list
-> (term -> truth) -> Proof.context -> conv
val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
@@ -435,7 +435,7 @@
{ ctxt = ctxt, consts = [] }
(K (fn ctxt' => fn t =>
case checked_computation cTs raw_computation ctxt' t of
- SOME x => conv x
+ SOME x => conv ctxt' x
| NONE => Conv.all_conv)));
in fn ctxt' => preprocess ctxt' then_conv computation_conv ctxt' end;
@@ -451,7 +451,7 @@
fun mount_computation_check ctxt cTs raw_computation =
mount_computation_conv ctxt cTs @{typ prop} raw_computation
- (K holds_oracle);
+ ((K o K) holds_oracle);
end;